Theorem r19.41v 2662

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-rex 2490

This theorem is referenced by:  r19.42v  2663  3reeanv  2677  reuind  2978  iuncom4  3934  dfiun2g  3959  iunxiun  4009  inuni  4199  xpiundi  4733  xpiundir  4734  imaco  5188  coiun  5192  abrexco  5828  imaiun  5829  isoini  5887  rexrnmpo  6061  mapsnen  6903  genpassl  7637  genpassu  7638  4fvwrd4  10262  4sqlem12  12725  metrest  14978  trirec0xor  15984