Theorem 19.43 1883

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 844	. . . 4 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
2	1	exbii 1848	. . 3 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ ∃𝑥(¬ 𝜑 → 𝜓))
3		19.35 1878	. . 3 ⊢ (∃𝑥(¬ 𝜑 → 𝜓) ↔ (∀𝑥 ¬ 𝜑 → ∃𝑥𝜓))
4		alnex 1782	. . . 4 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
5	4	imbi1i 352	. . 3 ⊢ ((∀𝑥 ¬ 𝜑 → ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
6	2, 3, 5	3bitri 299	. 2 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
7		df-or 844	. 2 ⊢ ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
8	6, 7	bitr4i 280	1 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∨ wo 843  ∀wal 1535  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 209  df-or 844  df-ex 1781

This theorem is referenced by:  19.34  1993  19.44v  1999  19.45v  2000  19.44  2239  19.45  2240  rexun  4166  unipr  4855  uniun  4861  unopab  5145  zfpair  5322  dmun  5779  dmopab2rex  5786  coundi  6100  coundir  6101  kmlem16  9591  vdwapun  16310  satfdm  32616  satf0op  32624  dmopab3rexdif  32652  bj-nnfor  34079  bj-nnford  34080  pm10.42  40716