\fo\imp分配左侧\ex(右侧无关)
theorem fo_imp_distls_ex_nfrs {x: set} (A B: wff x):
$ \nf x B $ >
$ \fo x (A \imp B) \iff \ex x A \imp B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | (\fo x (A \imp B) \imp \ex x A \imp B) \imp ((\ex x A \imp B) \imp \fo x (A \imp B)) \imp (\fo x (A \imp B) \iff \ex x A \imp B) |
|
| 2 | imp_iff_tran_imp | (\fo x (A \imp B) \imp \ex x A \imp \ex x B) \imp (\ex x A \imp \ex x B \iff \ex x A \imp B) \imp \fo x (A \imp B) \imp \ex x A \imp B |
|
| 3 | fo_imp_insto_ex | \fo x (A \imp B) \imp \ex x A \imp \ex x B |
|
| 4 | 2, 3 | ax_mp | (\ex x A \imp \ex x B \iff \ex x A \imp B) \imp \fo x (A \imp B) \imp \ex x A \imp B |
| 5 | iff_introl_imp | (\ex x B \iff B) \imp (\ex x A \imp \ex x B \iff \ex x A \imp B) |
|
| 6 | iff_symm | (B \iff \ex x B) \imp (\ex x B \iff B) |
|
| 7 | hyp n | \nf x B |
|
| 8 | 7 | ex_alloc_nf | B \iff \ex x B |
| 9 | 6, 8 | ax_mp | \ex x B \iff B |
| 10 | 5, 9 | ax_mp | \ex x A \imp \ex x B \iff \ex x A \imp B |
| 11 | 4, 10 | ax_mp | \fo x (A \imp B) \imp \ex x A \imp B |
| 12 | 1, 11 | ax_mp | ((\ex x A \imp B) \imp \fo x (A \imp B)) \imp (\fo x (A \imp B) \iff \ex x A \imp B) |
| 13 | imp_tran | ((\ex x A \imp B) \imp \ex x A \imp \fo x B) \imp ((\ex x A \imp \fo x B) \imp \fo x (A \imp B)) \imp (\ex x A \imp B) \imp \fo x (A \imp B) |
|
| 14 | imp_introl_imp | (B \imp \fo x B) \imp (\ex x A \imp B) \imp \ex x A \imp \fo x B |
|
| 15 | 7 | fo_intro_nf | B \imp \fo x B |
| 16 | 14, 15 | ax_mp | (\ex x A \imp B) \imp \ex x A \imp \fo x B |
| 17 | 13, 16 | ax_mp | ((\ex x A \imp \fo x B) \imp \fo x (A \imp B)) \imp (\ex x A \imp B) \imp \fo x (A \imp B) |
| 18 | ex_imp_fo_extto_fo | (\ex x A \imp \fo x B) \imp \fo x (A \imp B) |
|
| 19 | 17, 18 | ax_mp | (\ex x A \imp B) \imp \fo x (A \imp B) |
| 20 | 12, 19 | ax_mp | \fo x (A \imp B) \iff \ex x A \imp B |