Theorem 19.43 1915

Description: Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)

Assertion

Ref	Expression
19.43	⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))

Proof of Theorem 19.43

Step	Hyp	Ref	Expression
1		df-or 862	. . . 4 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
2	1	exbii 1881	. . 3 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ ∃𝑥(¬ 𝜑 → 𝜓))
3		19.35 1910	. . 3 ⊢ (∃𝑥(¬ 𝜑 → 𝜓) ↔ (∀𝑥 ¬ 𝜑 → ∃𝑥𝜓))
4		alnex 1814	. . . 4 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
5	4	imbi1i 352	. . 3 ⊢ ((∀𝑥 ¬ 𝜑 → ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
6	2, 3, 5	3bitri 300	. 2 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
7		df-or 862	. 2 ⊢ ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
8	6, 7	bitr4i 281	1 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813

This theorem is used by:  19.34  2025  19.44v  2031  19.45v  2032  19.44  2273  19.45  2274  eeor  2363  rexun  4142  uniprg  4883  uniun  4890  unopab  5185  zfpair  5386  dmun  5894  dmopab2rex  5901  coundi  6243  coundir  6244  kmlem16  10168  vdwapun  17066  satfdm  35948  satf0op  35956  dmopab3rexdif  35984  bj-nnfor  37489  bj-nnford  37490  bj-axseprep  37819  exor  43513  pm10.42  45188