Theorem r19.43 3139

Description: Restricted quantifier version of 19.43 1909. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
r19.43	⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))

Proof of Theorem r19.43

Step	Hyp	Ref	Expression
1		r19.35 3129	. 2 ⊢ (∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
2		df-or 861	. . 3 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
3	2	rexbii 3118	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓))
4		df-or 861	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
5		ralnex 3097	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
6	5	imbi1i 352	. . 3 ⊢ ((∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
7	4, 6	bitr4i 281	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
8	1, 3, 7	3bitr4i 306	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 860  ∀wral 3085  ∃wrex 3095

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-ral 3086  df-rex 3096

This theorem is referenced by:  3r19.43  3140  r19.45v  3205  r19.44v  3206  r19.45zv  4474  r19.44zv  4475  iunun  5063  soseq  8154  wemapsolem  9511  pythagtriplem2  16876  pythagtrip  16893  dcubic  26976  addsdilem1  28309  mulsasslem2  28322  legtrid  28825  axcontlem4  29257  erdszelem11  35591  satfvsucsuc  35755  fmla1  35777  seglelin  36506  hashnexinjle  42785  fimgmcyclem  43192  rexor  43291  diophun  43395  rexzrexnn0  43422  nprmmul3  48166  dfvopnbgr2  48506  dfsclnbgr6  48511  ldepslinc  49173