\ex\imp分配成\fo\ex
theorem ex_imp_distto_fo_ex {x: set} (A B: wff x):
$ \ex x (A \imp B) \iff \fo x A \imp \ex x B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | (\ex x (A \imp B) \imp \fo x A \imp \ex x B) \imp ((\fo x A \imp \ex x B) \imp \ex x (A \imp B)) \imp (\ex x (A \imp B) \iff \fo x A \imp \ex x B) |
|
| 2 | imp_imp_swapl | (\fo x A \imp \ex x (A \imp B) \imp \ex x B) \imp \ex x (A \imp B) \imp \fo x A \imp \ex x B |
|
| 3 | imp_tran | (\fo x A \imp \fo x ((A \imp B) \imp B)) \imp (\fo x ((A \imp B) \imp B) \imp \ex x (A \imp B) \imp \ex x B) \imp \fo x A \imp \ex x (A \imp B) \imp \ex x B |
|
| 4 | mp_hswap_thm | A \imp (A \imp B) \imp B |
|
| 5 | 4 | imp_intro_fo | \fo x A \imp \fo x ((A \imp B) \imp B) |
| 6 | 3, 5 | ax_mp | (\fo x ((A \imp B) \imp B) \imp \ex x (A \imp B) \imp \ex x B) \imp \fo x A \imp \ex x (A \imp B) \imp \ex x B |
| 7 | fo_imp_insto_ex | \fo x ((A \imp B) \imp B) \imp \ex x (A \imp B) \imp \ex x B |
|
| 8 | 6, 7 | ax_mp | \fo x A \imp \ex x (A \imp B) \imp \ex x B |
| 9 | 2, 8 | ax_mp | \ex x (A \imp B) \imp \fo x A \imp \ex x B |
| 10 | 1, 9 | ax_mp | ((\fo x A \imp \ex x B) \imp \ex x (A \imp B)) \imp (\ex x (A \imp B) \iff \fo x A \imp \ex x B) |
| 11 | neg_imp_with_imp_mergel_imp | (\neg \fo x A \imp \ex x (A \imp B)) \imp (\ex x B \imp \ex x (A \imp B)) \imp (\fo x A \imp \ex x B) \imp \ex x (A \imp B) |
|
| 12 | iff_imp_tran_imp | (\neg \fo x A \iff \ex x \neg A) \imp (\ex x \neg A \imp \ex x (A \imp B)) \imp \neg \fo x A \imp \ex x (A \imp B) |
|
| 13 | iff_symm | (\ex x \neg A \iff \neg \fo x A) \imp (\neg \fo x A \iff \ex x \neg A) |
|
| 14 | exneg_eqv_negfo | \ex x \neg A \iff \neg \fo x A |
|
| 15 | 13, 14 | ax_mp | \neg \fo x A \iff \ex x \neg A |
| 16 | 12, 15 | ax_mp | (\ex x \neg A \imp \ex x (A \imp B)) \imp \neg \fo x A \imp \ex x (A \imp B) |
| 17 | neg_elimintror_imp | \neg A \imp A \imp B |
|
| 18 | 17 | imp_intro_ex | \ex x \neg A \imp \ex x (A \imp B) |
| 19 | 16, 18 | ax_mp | \neg \fo x A \imp \ex x (A \imp B) |
| 20 | 11, 19 | ax_mp | (\ex x B \imp \ex x (A \imp B)) \imp (\fo x A \imp \ex x B) \imp \ex x (A \imp B) |
| 21 | introl_imp | B \imp A \imp B |
|
| 22 | 21 | imp_intro_ex | \ex x B \imp \ex x (A \imp B) |
| 23 | 20, 22 | ax_mp | (\fo x A \imp \ex x B) \imp \ex x (A \imp B) |
| 24 | 10, 23 | ax_mp | \ex x (A \imp B) \iff \fo x A \imp \ex x B |