Theorem r19.41v 2764

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

Assertion

Ref	Expression
r19.41v	⊢ (∃x ∈ A (φ ∧ ψ) ↔ (∃x ∈ A φ ∧ ψ))

Distinct variable group:   ψ,x

Allowed substitution hints:   φ(x)   A(x)

Proof of Theorem r19.41v

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 ⊢ Ⅎxψ
2	1	r19.41 2763	1 ⊢ (∃x ∈ A (φ ∧ ψ) ↔ (∃x ∈ A φ ∧ ψ))

Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wrex 2615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-rex 2620

This theorem is referenced by:  r19.42v  2765  3reeanv  2779  reuind  3039  iuncom4  3976  dfiun2g  3999  iunxiun  4048  elpw12  4145  pw1in  4164  imacok  4282  unipw1  4325  dfaddc2  4381  addcass  4415  ltfinex  4464  ncfinlowerlem1  4482  dfevenfin2  4512  dfoddfin2  4513  nnpweqlem1  4522  vfinspss  4551  vfinncsp  4554  phialllem1  4616  setconslem6  4736  xpiundi  4817  xpiundir  4818  elimapw1  4944  elimapw12  4945  elimapw13  4946  imaco  5086  coiun  5090  abrexco  5463  imaiun  5464  isomin  5496  isoini  5497  xpassen  6057  enpw1pw  6075