Theorem r19.41v 2587

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 1508	. 2 ⊢ Ⅎ𝑥𝜓
2	1	r19.41 2586	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ∧ wa 103   ↔ wb 104  ∃wrex 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-rex 2422

This theorem is referenced by:  r19.42v  2588  3reeanv  2601  reuind  2889  iuncom4  3820  dfiun2g  3845  iunxiun  3894  inuni  4080  xpiundi  4597  xpiundir  4598  imaco  5044  coiun  5048  abrexco  5660  imaiun  5661  isoini  5719  rexrnmpo  5886  mapsnen  6705  genpassl  7332  genpassu  7333  4fvwrd4  9917  metrest  12675