\ex\imp分配左侧\fo(右侧无关)
theorem ex_imp_distls_fo_nfrs {x: set} (A B: wff x):
$ \nf x B $ >
$ \ex x (A \imp B) \iff \fo x A \imp B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_tran | (\ex x (A \imp B) \iff \fo x A \imp \ex x B) \imp (\fo x A \imp \ex x B \iff \fo x A \imp B) \imp (\ex x (A \imp B) \iff \fo x A \imp B) |
|
| 2 | ex_imp_distto_fo_ex | \ex x (A \imp B) \iff \fo x A \imp \ex x B |
|
| 3 | 1, 2 | ax_mp | (\fo x A \imp \ex x B \iff \fo x A \imp B) \imp (\ex x (A \imp B) \iff \fo x A \imp B) |
| 4 | iff_introl_imp | (\ex x B \iff B) \imp (\fo x A \imp \ex x B \iff \fo x A \imp B) |
|
| 5 | iff_symm | (B \iff \ex x B) \imp (\ex x B \iff B) |
|
| 6 | hyp n | \nf x B |
|
| 7 | 6 | ex_alloc_nf | B \iff \ex x B |
| 8 | 5, 7 | ax_mp | \ex x B \iff B |
| 9 | 4, 8 | ax_mp | \fo x A \imp \ex x B \iff \fo x A \imp B |
| 10 | 3, 9 | ax_mp | \ex x (A \imp B) \iff \fo x A \imp B |