Theorem rspe 2556

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 2491	. 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 2177   E.wrex 2486

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 2491

This theorem is referenced by:  rsp2e  2558  ssiun2  3976  tfrlem9  6418  tfrlemibxssdm  6426  tfr1onlembxssdm  6442  tfrcllembxssdm  6455  findcard2  7001  findcard2s  7002  prarloclemup  7628  prmuloc2  7700  ltaddpr  7730  aptiprlemu  7773  cauappcvgprlemopl  7779  cauappcvgprlemopu  7781  cauappcvgprlem2  7793  caucvgprlemopl  7802  caucvgprlemopu  7804  caucvgprlem2  7813  caucvgprprlem2  7843  suplocexprlemrl  7850  suplocexprlemru  7852  suplocexprlemlub  7857