Theorem r19.41v 2707

Description: Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 17-Dec-2003.)

Assertion

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

Distinct variable group:   𝜓,𝑥

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

Proof of Theorem r19.41v

Step	Hyp	Ref	Expression
1		nfv 1581	. 2 ⊢ Ⅎ𝑥𝜓
2	1	r19.41 2706	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-rex 2534

This theorem is referenced by:  r19.42v  2708  3reeanv  2722  reuind  3031  iuncom4  4014  dfiun2g  4039  iunxiun  4089  inuni  4286  xpiundi  4828  xpiundir  4829  imaco  5288  coiun  5292  abrexco  5955  imaiun  5956  isoini  6014  rexrnmpo  6194  mapsnend  7089  mapsnen  7090  genpassl  7881  genpassu  7882  4fvwrd4  10525  4sqlem12  13159  metrest  15530  trirec0xor  16999