Theorem rspe 2543

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 1601	. 2 |- ( ( x e. A /\ ph ) -> E. x ( x e. A /\ ph ) )
2		df-rex 2478	. 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 1503   e. wcel 2164   E.wrex 2473

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 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521

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

This theorem is referenced by:  rsp2e  2545  ssiun2  3956  tfrlem9  6374  tfrlemibxssdm  6382  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  findcard2  6947  findcard2s  6948  prarloclemup  7557  prmuloc2  7629  ltaddpr  7659  aptiprlemu  7702  cauappcvgprlemopl  7708  cauappcvgprlemopu  7710  cauappcvgprlem2  7722  caucvgprlemopl  7731  caucvgprlemopu  7733  caucvgprlem2  7742  caucvgprprlem2  7772  suplocexprlemrl  7779  suplocexprlemru  7781  suplocexprlemlub  7786