Theorem r19.41v 2466

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 1421	. 2 |- F/ x ps
2	1	r19.41 2465	1 |- ( E. x e. A ( ph /\ ps ) <-> ( E. x e. A ph /\ ps ) )

Syntax hints:   /\ wa 97   <-> wb 98   E.wrex 2307

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-rex 2312

This theorem is referenced by:  r19.42v  2467  3reeanv  2480  reuind  2744  iuncom4  3664  dfiun2g  3689  iunxiun  3736  inuni  3909  xpiundi  4398  xpiundir  4399  imaco  4826  coiun  4830  abrexco  5398  imaiun  5399  isoini  5457  rexrnmpt2  5616  genpassl  6622  genpassu  6623  4fvwrd4  8997