Theorem r19.41v 2610

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-17 1503  ax-ial 1511

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-rex 2438

This theorem is referenced by:  r19.42v  2611  3reeanv  2624  reuind  2913  iuncom4  3852  dfiun2g  3877  iunxiun  3926  inuni  4112  xpiundi  4637  xpiundir  4638  imaco  5084  coiun  5088  abrexco  5700  imaiun  5701  isoini  5759  rexrnmpo  5926  mapsnen  6745  genpassl  7423  genpassu  7424  4fvwrd4  10017  metrest  12853  trirec0xor  13565