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  3923  dfiun2g  3948  iunxiun  3998  inuni  4188  xpiundi  4721  xpiundir  4722  imaco  5175  coiun  5179  abrexco  5806  imaiun  5807  isoini  5865  rexrnmpo  6038  mapsnen  6870  genpassl  7591  genpassu  7592  4fvwrd4  10215  4sqlem12  12571  metrest  14742  trirec0xor  15689