\fo\or插入成\ex\fo
theorem fo_or_insto_ex_fo {x: set} (A B: wff x):
$ \fo x (A \or B) \imp \ex x A \or \fo x B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_iff_tran_imp | (\fo x (A \or B) \imp \fo x B \or \ex x A) \imp (\fo x B \or \ex x A \iff \ex x A \or \fo x B) \imp \fo x (A \or B) \imp \ex x A \or \fo x B |
|
| 2 | iff_imp_tran_imp | (\fo x (A \or B) \iff \fo x (B \or A)) \imp (\fo x (B \or A) \imp \fo x B \or \ex x A) \imp \fo x (A \or B) \imp \fo x B \or \ex x A |
|
| 3 | or_comm | A \or B \iff B \or A |
|
| 4 | 3 | iff_intro_fo | \fo x (A \or B) \iff \fo x (B \or A) |
| 5 | 2, 4 | ax_mp | (\fo x (B \or A) \imp \fo x B \or \ex x A) \imp \fo x (A \or B) \imp \fo x B \or \ex x A |
| 6 | fo_or_insto_fo_ex | \fo x (B \or A) \imp \fo x B \or \ex x A |
|
| 7 | 5, 6 | ax_mp | \fo x (A \or B) \imp \fo x B \or \ex x A |
| 8 | 1, 7 | ax_mp | (\fo x B \or \ex x A \iff \ex x A \or \fo x B) \imp \fo x (A \or B) \imp \ex x A \or \fo x B |
| 9 | or_comm | \fo x B \or \ex x A \iff \ex x A \or \fo x B |
|
| 10 | 8, 9 | ax_mp | \fo x (A \or B) \imp \ex x A \or \fo x B |