Theorem r19.42v 2665

Description: Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)

Assertion

Ref	Expression
r19.42v	⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.42v

Step	Hyp	Ref	Expression
1		r19.41v 2664	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 266	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 2515	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 266	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 212	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ∧ wa 104   ↔ wb 105  ∃wrex 2487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-rex 2492

This theorem is referenced by:  ceqsrexbv  2911  ceqsrex2v  2912  2reuswapdc  2984  iunrab  3989  iunin2  4005  iundif2ss  4007  iunopab  4346  elxp2  4711  cnvuni  4882  elunirn  5858  f1oiso  5918  oprabrexex2  6238  genpdflem  7655  1idprl  7738  1idpru  7739  ltexprlemm  7748  rexuz2  9737  4fvwrd4  10297  divalgb  12351