Theorem r19.41v 2559

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

Syntax hints:   /\ wa 103   <-> wb 104   E.wrex 2389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-rex 2394

This theorem is referenced by:  r19.42v  2560  3reeanv  2573  reuind  2856  iuncom4  3784  dfiun2g  3809  iunxiun  3858  inuni  4038  xpiundi  4555  xpiundir  4556  imaco  5000  coiun  5004  abrexco  5612  imaiun  5613  isoini  5671  rexrnmpo  5838  mapsnen  6657  genpassl  7274  genpassu  7275  4fvwrd4  9804  metrest  12489