Theorem r19.41v 2511

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

Syntax hints:   ∧ wa 102   ↔ wb 103  ∃wrex 2350

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-rex 2355

This theorem is referenced by:  r19.42v  2512  3reeanv  2525  reuind  2796  iuncom4  3693  dfiun2g  3718  iunxiun  3765  inuni  3938  xpiundi  4424  xpiundir  4425  imaco  4856  coiun  4860  abrexco  5430  imaiun  5431  isoini  5488  rexrnmpt2  5647  genpassl  6776  genpassu  6777  4fvwrd4  9227