Theorem 19.43 1884

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 849	. . . 4 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
2	1	exbii 1850	. . 3 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ ∃𝑥(¬ 𝜑 → 𝜓))
3		19.35 1879	. . 3 ⊢ (∃𝑥(¬ 𝜑 → 𝜓) ↔ (∀𝑥 ¬ 𝜑 → ∃𝑥𝜓))
4		alnex 1783	. . . 4 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
5	4	imbi1i 349	. . 3 ⊢ ((∀𝑥 ¬ 𝜑 → ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
6	2, 3, 5	3bitri 297	. 2 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
7		df-or 849	. 2 ⊢ ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
8	6, 7	bitr4i 278	1 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 848  ∀wal 1540  ∃wex 1781

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

This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1782

This theorem is referenced by:  19.34  1994  19.44v  2000  19.45v  2001  19.44  2245  19.45  2246  eeor  2339  rexun  4137  uniprg  4867  uniun  4874  unopab  5166  zfpair  5358  dmun  5859  dmopab2rex  5866  coundi  6205  coundir  6206  kmlem16  10079  vdwapun  16936  satfdm  35567  satf0op  35575  dmopab3rexdif  35603  bj-nnfor  37069  bj-nnford  37070  bj-axseprep  37397  exor  43114  pm10.42  44809