Theorem r19.42v 2708

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 2707	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 266	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 2557	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 266	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 212	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-rex 2534

This theorem is used by:  ceqsrexbv  2957  ceqsrex2v  2958  2reuswapdc  3030  iunrab  4060  iunin2  4076  iundif2ss  4078  iunopab  4424  elxp2  4792  cnvuni  4966  elunirn  5972  f1oiso  6032  oprabrexex2  6363  genpdflem  7874  1idprl  7957  1idpru  7958  ltexprlemm  7967  rexuz2  9981  4fvwrd4  10547  divalgb  12692