Theorem rspe 2554

Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.)

Assertion

Ref	Expression
rspe	|- ( ( x e. A /\ ph ) -> E. x e. A ph )

Proof of Theorem rspe

Step	Hyp	Ref	Expression
1		19.8a 1612	. 2 |- ( ( x e. A /\ ph ) -> E. x ( x e. A /\ ph ) )
2		df-rex 2489	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
3	1, 2	sylibr 134	1 |- ( ( x e. A /\ ph ) -> E. x e. A ph )

Syntax hints:   -> wi 4   /\ wa 104   E.wex 1514   e. wcel 2175   E.wrex 2484

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-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532

This theorem depends on definitions:  df-bi 117  df-rex 2489

This theorem is referenced by:  rsp2e  2556  ssiun2  3969  tfrlem9  6395  tfrlemibxssdm  6403  tfr1onlembxssdm  6419  tfrcllembxssdm  6432  findcard2  6968  findcard2s  6969  prarloclemup  7590  prmuloc2  7662  ltaddpr  7692  aptiprlemu  7735  cauappcvgprlemopl  7741  cauappcvgprlemopu  7743  cauappcvgprlem2  7755  caucvgprlemopl  7764  caucvgprlemopu  7766  caucvgprlem2  7775  caucvgprprlem2  7805  suplocexprlemrl  7812  suplocexprlemru  7814  suplocexprlemlub  7819