Theorem r19.41v 2590

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

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

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-rex 2423

This theorem is referenced by:  r19.42v  2591  3reeanv  2604  reuind  2893  iuncom4  3828  dfiun2g  3853  iunxiun  3902  inuni  4088  xpiundi  4605  xpiundir  4606  imaco  5052  coiun  5056  abrexco  5668  imaiun  5669  isoini  5727  rexrnmpo  5894  mapsnen  6713  genpassl  7356  genpassu  7357  4fvwrd4  9948  metrest  12714  trirec0xor  13413