Theorem r19.43 3135

Description: Restricted quantifier version of 19.43 1915. (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 3125	. 2 ⊢ (∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
2		df-or 862	. . 3 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
3	2	rexbii 3114	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓))
4		df-or 862	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
5		ralnex 3093	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
6	5	imbi1i 352	. . 3 ⊢ ((∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
7	4, 6	bitr4i 281	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
8	1, 3, 7	3bitr4i 306	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861  ∀wral 3081  ∃wrex 3091

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-an 402  df-or 862  df-ex 1813  df-ral 3082  df-rex 3092

This theorem is used by:  3r19.43  3136  r19.45v  3201  r19.44v  3202  r19.45zv  4471  r19.44zv  4472  iunun  5061  soseq  8161  wemapsolem  9519  pythagtriplem2  16899  pythagtrip  16916  dcubic  27062  addsdilem1  28395  mulsasslem2  28408  legtrid  28911  axcontlem4  29372  erdszelem11  35730  satfvsucsuc  35894  fmla1  35916  seglelin  36645  hashnexinjle  42954  fimgmcyclem  43359  rexor  43458  diophun  43562  rexzrexnn0  43589  nprmmul3  48336  dfvopnbgr2  48676  dfsclnbgr6  48681  ldepslinc  49346