Theorem rspe 2557

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 1614	. 2 |- ( ( x e. A /\ ph ) -> E. x ( x e. A /\ ph ) )
2		df-rex 2492	. 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 1516   e. wcel 2178   E.wrex 2487

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 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534

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

This theorem is referenced by:  rsp2e  2559  ssiun2  3984  tfrlem9  6428  tfrlemibxssdm  6436  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  findcard2  7012  findcard2s  7013  prarloclemup  7643  prmuloc2  7715  ltaddpr  7745  aptiprlemu  7788  cauappcvgprlemopl  7794  cauappcvgprlemopu  7796  cauappcvgprlem2  7808  caucvgprlemopl  7817  caucvgprlemopu  7819  caucvgprlem2  7828  caucvgprprlem2  7858  suplocexprlemrl  7865  suplocexprlemru  7867  suplocexprlemlub  7872