Theorem r19.41v 2650

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 2649	1 |- ( E. x e. A ( ph /\ ps ) <-> ( E. x e. A ph /\ ps ) )

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

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 2478

This theorem is referenced by:  r19.42v  2651  3reeanv  2665  reuind  2966  iuncom4  3920  dfiun2g  3945  iunxiun  3995  inuni  4185  xpiundi  4718  xpiundir  4719  imaco  5172  coiun  5176  abrexco  5803  imaiun  5804  isoini  5862  rexrnmpo  6035  mapsnen  6867  genpassl  7586  genpassu  7587  4fvwrd4  10209  4sqlem12  12543  metrest  14685  trirec0xor  15605