Theorem r19.41v 2622

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

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

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-rex 2450

This theorem is referenced by:  r19.42v  2623  3reeanv  2636  reuind  2931  iuncom4  3873  dfiun2g  3898  iunxiun  3947  inuni  4134  xpiundi  4662  xpiundir  4663  imaco  5109  coiun  5113  abrexco  5727  imaiun  5728  isoini  5786  rexrnmpo  5957  mapsnen  6777  genpassl  7465  genpassu  7466  4fvwrd4  10075  metrest  13146  trirec0xor  13924