Theorem rspe 2524

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 1588	. 2 |- ( ( x e. A /\ ph ) -> E. x ( x e. A /\ ph ) )
2		df-rex 2459	. 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 1490   e. wcel 2146   E.wrex 2454

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 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508

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

This theorem is referenced by:  rsp2e  2526  ssiun2  3925  tfrlem9  6310  tfrlemibxssdm  6318  tfr1onlembxssdm  6334  tfrcllembxssdm  6347  findcard2  6879  findcard2s  6880  prarloclemup  7469  prmuloc2  7541  ltaddpr  7571  aptiprlemu  7614  cauappcvgprlemopl  7620  cauappcvgprlemopu  7622  cauappcvgprlem2  7634  caucvgprlemopl  7643  caucvgprlemopu  7645  caucvgprlem2  7654  caucvgprprlem2  7684  suplocexprlemrl  7691  suplocexprlemru  7693  suplocexprlemlub  7698