Theorem rspe 2582

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 1639	. 2 |- ( ( x e. A /\ ph ) -> E. x ( x e. A /\ ph ) )
2		df-rex 2517	. 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 1541   e. wcel 2202   E.wrex 2512

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 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559

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

This theorem is referenced by:  rsp2e  2584  ssiun2  4018  tfrlem9  6528  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  findcard2  7121  findcard2s  7122  prarloclemup  7758  prmuloc2  7830  ltaddpr  7860  aptiprlemu  7903  cauappcvgprlemopl  7909  cauappcvgprlemopu  7911  cauappcvgprlem2  7923  caucvgprlemopl  7932  caucvgprlemopu  7934  caucvgprlem2  7943  caucvgprprlem2  7973  suplocexprlemrl  7980  suplocexprlemru  7982  suplocexprlemlub  7987