Theorem r19.41v 2662

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-rex 2490

This theorem is referenced by:  r19.42v  2663  3reeanv  2677  reuind  2978  iuncom4  3934  dfiun2g  3959  iunxiun  4009  inuni  4200  xpiundi  4734  xpiundir  4735  imaco  5189  coiun  5193  abrexco  5830  imaiun  5831  isoini  5889  rexrnmpo  6063  mapsnen  6905  genpassl  7639  genpassu  7640  4fvwrd4  10264  4sqlem12  12758  metrest  15011  trirec0xor  16021