Theorem r19.43 3104

Description: Restricted quantifier version of 19.43 1883. (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 3094	. 2 ⊢ (∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
2		df-or 848	. . 3 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
3	2	rexbii 3083	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓))
4		df-or 848	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
5		ralnex 3062	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
6	5	imbi1i 349	. . 3 ⊢ ((∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
7	4, 6	bitr4i 278	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
8	1, 3, 7	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 847  ∀wral 3051  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-ral 3052  df-rex 3061

This theorem is referenced by:  3r19.43  3105  r19.45v  3170  r19.44v  3171  r19.45zv  4461  r19.44zv  4462  iunun  5048  soseq  8101  wemapsolem  9455  pythagtriplem2  16745  pythagtrip  16762  dcubic  26812  addsdilem1  28147  mulsasslem2  28160  legtrid  28663  axcontlem4  29040  erdszelem11  35395  satfvsucsuc  35559  fmla1  35581  seglelin  36310  hashnexinjle  42383  fimgmcyclem  42788  rexor  42911  diophun  43015  rexzrexnn0  43046  dfvopnbgr2  48099  dfsclnbgr6  48104  ldepslinc  48755