Theorem rspe 2599

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 1643	. 2 |- ( ( x e. A /\ ph ) -> E. x ( x e. A /\ ph ) )
2		df-rex 2534	. 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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   E.wex 1545   e. wcel 2209   E.wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563

This proof depends on definitions:  df-bi 117  df-rex 2534

This theorem is used by:  rsp2e  2601  ssiun2  4055  tfrlem9  6590  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  findcard2  7193  findcard2s  7194  prarloclemup  7863  prmuloc2  7935  ltaddpr  7965  aptiprlemu  8008  cauappcvgprlemopl  8014  cauappcvgprlemopu  8016  cauappcvgprlem2  8028  caucvgprlemopl  8037  caucvgprlemopu  8039  caucvgprlem2  8048  caucvgprprlem2  8078  suplocexprlemrl  8085  suplocexprlemru  8087  suplocexprlemlub  8092  bposlem3  16274