Theorem r19.41v 2481

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

Syntax hints:   ∧ wa 101   ↔ wb 102  ∃wrex 2322

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-4 1414  ax-17 1433  ax-ial 1441

This theorem depends on definitions:  df-bi 114  df-nf 1364  df-rex 2327

This theorem is referenced by:  r19.42v  2482  3reeanv  2495  reuind  2764  iuncom4  3689  dfiun2g  3714  iunxiun  3761  inuni  3934  xpiundi  4423  xpiundir  4424  imaco  4851  coiun  4855  abrexco  5423  imaiun  5424  isoini  5482  rexrnmpt2  5641  genpassl  6650  genpassu  6651  4fvwrd4  9069