Theorem 19.43 1917

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 1912	. . 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  2027  19.44v  2033  19.45v  2034  19.44  2277  19.45  2278  eeor  2367  rexun  4197  uniprg  4888  uniun  4895  unopab  5191  zfpair  5390  dmun  5904  dmopab2rex  5911  coundi  6267  coundir  6268  kmlem16  10283  vdwapun  17196  onprcf1of1ord  36096  satfdm  36342  satf0op  36350  dmopab3rexdif  36378  bj-nnfor  37873  bj-nnford  37874  bj-axseprep  38260  exor  43944  pm10.42  45609