\ex\and分配左侧(右侧不出现)
theorem ex_and_distls_nfrs {x: set} (A B: wff x):
$ \nf x B $ >
$ \ex x (A \and B) \iff \ex x A \and B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | (\ex x (A \and B) \imp \ex x A \and B) \imp (\ex x A \and B \imp \ex x (A \and B)) \imp (\ex x (A \and B) \iff \ex x A \and B) |
|
| 2 | imp_tran | (\ex x (A \and B) \imp \ex x A \and \ex x B) \imp (\ex x A \and \ex x B \imp \ex x A \and B) \imp \ex x (A \and B) \imp \ex x A \and B |
|
| 3 | ex_and_ins | \ex x (A \and B) \imp \ex x A \and \ex x B |
|
| 4 | 2, 3 | ax_mp | (\ex x A \and \ex x B \imp \ex x A \and B) \imp \ex x (A \and B) \imp \ex x A \and B |
| 5 | imp_introl_and | (\ex x B \imp B) \imp \ex x A \and \ex x B \imp \ex x A \and B |
|
| 6 | hyp n | \nf x B |
|
| 7 | 6 | ex_elim_nf | \ex x B \imp B |
| 8 | 5, 7 | ax_mp | \ex x A \and \ex x B \imp \ex x A \and B |
| 9 | 4, 8 | ax_mp | \ex x (A \and B) \imp \ex x A \and B |
| 10 | 1, 9 | ax_mp | (\ex x A \and B \imp \ex x (A \and B)) \imp (\ex x (A \and B) \iff \ex x A \and B) |
| 11 | iff_imp_tran_imp | (\ex x A \and B \iff B \and \ex x A) \imp (B \and \ex x A \imp \ex x (A \and B)) \imp \ex x A \and B \imp \ex x (A \and B) |
|
| 12 | and_comm | \ex x A \and B \iff B \and \ex x A |
|
| 13 | 11, 12 | ax_mp | (B \and \ex x A \imp \ex x (A \and B)) \imp \ex x A \and B \imp \ex x (A \and B) |
| 14 | iff_eliml | (B \imp \ex x A \imp \ex x (A \and B) \iff B \and \ex x A \imp \ex x (A \and B)) \imp (B \imp \ex x A \imp \ex x (A \and B)) \imp B \and \ex x A \imp \ex x (A \and B) |
|
| 15 | imp_nested_gatherl_and | B \imp \ex x A \imp \ex x (A \and B) \iff B \and \ex x A \imp \ex x (A \and B) |
|
| 16 | 14, 15 | ax_mp | (B \imp \ex x A \imp \ex x (A \and B)) \imp B \and \ex x A \imp \ex x (A \and B) |
| 17 | imp_tran | (B \imp \fo x (A \imp A \and B)) \imp (\fo x (A \imp A \and B) \imp \ex x A \imp \ex x (A \and B)) \imp B \imp \ex x A \imp \ex x (A \and B) |
|
| 18 | imp_imp_swapl | (A \imp B \imp A \and B) \imp B \imp A \imp A \and B |
|
| 19 | and_comp | A \imp B \imp A \and B |
|
| 20 | 18, 19 | ax_mp | B \imp A \imp A \and B |
| 21 | 6, 20 | imp_intrors_fo_nfls | B \imp \fo x (A \imp A \and B) |
| 22 | 17, 21 | ax_mp | (\fo x (A \imp A \and B) \imp \ex x A \imp \ex x (A \and B)) \imp B \imp \ex x A \imp \ex x (A \and B) |
| 23 | fo_imp_insto_ex | \fo x (A \imp A \and B) \imp \ex x A \imp \ex x (A \and B) |
|
| 24 | 22, 23 | ax_mp | B \imp \ex x A \imp \ex x (A \and B) |
| 25 | 16, 24 | ax_mp | B \and \ex x A \imp \ex x (A \and B) |
| 26 | 13, 25 | ax_mp | \ex x A \and B \imp \ex x (A \and B) |
| 27 | 10, 26 | ax_mp | \ex x (A \and B) \iff \ex x A \and B |