Theorem 19.43 1886

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 847	. . . 4 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
2	1	exbii 1851	. . 3 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ ∃𝑥(¬ 𝜑 → 𝜓))
3		19.35 1881	. . 3 ⊢ (∃𝑥(¬ 𝜑 → 𝜓) ↔ (∀𝑥 ¬ 𝜑 → ∃𝑥𝜓))
4		alnex 1784	. . . 4 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
5	4	imbi1i 350	. . 3 ⊢ ((∀𝑥 ¬ 𝜑 → ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
6	2, 3, 5	3bitri 297	. 2 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
7		df-or 847	. 2 ⊢ ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
8	6, 7	bitr4i 278	1 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∨ wo 846  ∀wal 1540  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-or 847  df-ex 1783

This theorem is referenced by:  19.34  1991  19.44v  1997  19.45v  1998  19.44  2231  19.45  2232  eeor  2330  rexun  4191  uniprg  4926  uniprOLD  4928  uniun  4935  unopab  5231  zfpair  5420  dmun  5911  dmopab2rex  5918  coundi  6247  coundir  6248  kmlem16  10160  vdwapun  16907  satfdm  34360  satf0op  34368  dmopab3rexdif  34396  bj-nnfor  35628  bj-nnford  35629  pm10.42  43123