Theorem r19.41v 2653

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-rex 2481

This theorem is referenced by:  r19.42v  2654  3reeanv  2668  reuind  2969  iuncom4  3924  dfiun2g  3949  iunxiun  3999  inuni  4189  xpiundi  4722  xpiundir  4723  imaco  5176  coiun  5180  abrexco  5809  imaiun  5810  isoini  5868  rexrnmpo  6042  mapsnen  6879  genpassl  7608  genpassu  7609  4fvwrd4  10232  4sqlem12  12596  metrest  14826  trirec0xor  15776