Theorem r19.41v 2707

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

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-rex 2534

This theorem is referenced by:  r19.42v  2708  3reeanv  2722  reuind  3031  iuncom4  4017  dfiun2g  4042  iunxiun  4092  inuni  4289  xpiundi  4831  xpiundir  4832  imaco  5291  coiun  5295  abrexco  5958  imaiun  5959  isoini  6017  rexrnmpo  6197  mapsnend  7092  mapsnen  7093  genpassl  7884  genpassu  7885  4fvwrd4  10528  4sqlem12  13162  metrest  15533  trirec0xor  17002