\ex\and分配右侧(左侧不出现)
theorem ex_and_distrs_nfls {x: set} (A B: wff x):
$ \nf x A $ >
$ \ex x (A \and B) \iff A \and \ex x B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_tran | (\ex x (A \and B) \iff \ex x B \and A) \imp (\ex x B \and A \iff A \and \ex x B) \imp (\ex x (A \and B) \iff A \and \ex x B) |
|
| 2 | iff_tran | (\ex x (A \and B) \iff \ex x (B \and A)) \imp (\ex x (B \and A) \iff \ex x B \and A) \imp (\ex x (A \and B) \iff \ex x B \and A) |
|
| 3 | and_comm | A \and B \iff B \and A |
|
| 4 | 3 | iff_intro_ex | \ex x (A \and B) \iff \ex x (B \and A) |
| 5 | 2, 4 | ax_mp | (\ex x (B \and A) \iff \ex x B \and A) \imp (\ex x (A \and B) \iff \ex x B \and A) |
| 6 | hyp n | \nf x A |
|
| 7 | 6 | ex_and_distls_nfrs | \ex x (B \and A) \iff \ex x B \and A |
| 8 | 5, 7 | ax_mp | \ex x (A \and B) \iff \ex x B \and A |
| 9 | 1, 8 | ax_mp | (\ex x B \and A \iff A \and \ex x B) \imp (\ex x (A \and B) \iff A \and \ex x B) |
| 10 | and_comm | \ex x B \and A \iff A \and \ex x B |
|
| 11 | 9, 10 | ax_mp | \ex x (A \and B) \iff A \and \ex x B |