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  7862  prmuloc2  7934  ltaddpr  7964  aptiprlemu  8007  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlem2  8027  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlem2  8047  caucvgprprlem2  8077  suplocexprlemrl  8084  suplocexprlemru  8086  suplocexprlemlub  8091