\ex\or分配
theorem ex_or_dist {x: set} (A B: wff x):
$ \ex x (A \or B) \iff \ex x A \or \ex x B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_tran | (\ex x (\neg A \imp B) \iff \fo x \neg A \imp \ex x B) \imp (\fo x \neg A \imp \ex x B \iff \neg \ex x A \imp \ex x B) \imp (\ex x (\neg A \imp B) \iff \neg \ex x A \imp \ex x B) |
|
| 2 | ex_imp_distto_fo_ex | \ex x (\neg A \imp B) \iff \fo x \neg A \imp \ex x B |
|
| 3 | 1, 2 | ax_mp | (\fo x \neg A \imp \ex x B \iff \neg \ex x A \imp \ex x B) \imp (\ex x (\neg A \imp B) \iff \neg \ex x A \imp \ex x B) |
| 4 | iff_intror_imp | (\fo x \neg A \iff \neg \ex x A) \imp (\fo x \neg A \imp \ex x B \iff \neg \ex x A \imp \ex x B) |
|
| 5 | foneg_eqv_negex | \fo x \neg A \iff \neg \ex x A |
|
| 6 | 4, 5 | ax_mp | \fo x \neg A \imp \ex x B \iff \neg \ex x A \imp \ex x B |
| 7 | 3, 6 | ax_mp | \ex x (\neg A \imp B) \iff \neg \ex x A \imp \ex x B |
| 8 | 7 | conv or | \ex x (A \or B) \iff \ex x A \or \ex x B |