Theorem r19.43 3130

Description: Restricted quantifier version of 19.43 1902. (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 3120	. 2 ⊢ (∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
2		df-or 859	. . 3 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
3	2	rexbii 3109	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓))
4		df-or 859	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
5		ralnex 3088	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
6	5	imbi1i 351	. . 3 ⊢ ((∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
7	4, 6	bitr4i 280	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
8	1, 3, 7	3bitr4i 305	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∨ wo 858  ∀wral 3076  ∃wrex 3086

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1800  df-ral 3077  df-rex 3087

This theorem is referenced by:  3r19.43  3131  r19.45v  3196  r19.44v  3197  r19.45zv  4462  r19.44zv  4463  iunun  5050  soseq  8139  wemapsolem  9498  pythagtriplem2  16853  pythagtrip  16870  dcubic  26911  addsdilem1  28244  mulsasslem2  28257  legtrid  28760  axcontlem4  29168  erdszelem11  35551  satfvsucsuc  35715  fmla1  35737  seglelin  36466  hashnexinjle  42746  fimgmcyclem  43151  rexor  43250  diophun  43354  rexzrexnn0  43381  nprmmul3  48135  dfvopnbgr2  48475  dfsclnbgr6  48480  ldepslinc  49131