Theorem rspe 2481

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 1569	. 2 |- ( ( x e. A /\ ph ) -> E. x ( x e. A /\ ph ) )
2		df-rex 2422	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
3	1, 2	sylibr 133	1 |- ( ( x e. A /\ ph ) -> E. x e. A ph )

Syntax hints:   -> wi 4   /\ wa 103   E.wex 1468   e. wcel 1480   E.wrex 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487

This theorem depends on definitions:  df-bi 116  df-rex 2422

This theorem is referenced by:  rsp2e  2483  ssiun2  3856  tfrlem9  6216  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  findcard2  6783  findcard2s  6784  prarloclemup  7303  prmuloc2  7375  ltaddpr  7405  aptiprlemu  7448  cauappcvgprlemopl  7454  cauappcvgprlemopu  7456  cauappcvgprlem2  7468  caucvgprlemopl  7477  caucvgprlemopu  7479  caucvgprlem2  7488  caucvgprprlem2  7518  suplocexprlemrl  7525  suplocexprlemru  7527  suplocexprlemlub  7532