Theorem r19.41v 2646

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

Syntax hints:   /\ wa 104   <-> wb 105   E.wrex 2469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-rex 2474

This theorem is referenced by:  r19.42v  2647  3reeanv  2661  reuind  2957  iuncom4  3908  dfiun2g  3933  iunxiun  3983  inuni  4173  xpiundi  4702  xpiundir  4703  imaco  5152  coiun  5156  abrexco  5781  imaiun  5782  isoini  5840  rexrnmpo  6012  mapsnen  6837  genpassl  7553  genpassu  7554  4fvwrd4  10170  4sqlem12  12434  metrest  14463  trirec0xor  15252