Theorem r19.41v 2765

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

Assertion

Ref	Expression
r19.41v	|- (E.x e. A (ph /\ ps) <-> (E.x e. A ph /\ ps))

Distinct variable group:   ps,x

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

Proof of Theorem r19.41v

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 |- F/xps
2	1	r19.41 2764	1 |- (E.x e. A (ph /\ ps) <-> (E.x e. A ph /\ ps))

Syntax hints:   <-> wb 176   /\ wa 358  E.wrex 2616

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 2621

This theorem is referenced by:  r19.42v  2766  3reeanv  2780  reuind  3040  iuncom4  3977  dfiun2g  4000  iunxiun  4049  elpw12  4146  pw1in  4165  imacok  4283  unipw1  4326  dfaddc2  4382  addcass  4416  ltfinex  4465  ncfinlowerlem1  4483  dfevenfin2  4513  dfoddfin2  4514  nnpweqlem1  4523  vfinspss  4552  vfinncsp  4555  phialllem1  4617  setconslem6  4737  xpiundi  4818  xpiundir  4819  elimapw1  4945  elimapw12  4946  elimapw13  4947  imaco  5087  coiun  5091  abrexco  5464  imaiun  5465  isomin  5497  isoini  5498  xpassen  6058  enpw1pw  6076