Theorem rspe 2484

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 1570	. 2 |- ( ( x e. A /\ ph ) -> E. x ( x e. A /\ ph ) )
2		df-rex 2423	. 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 1469   e. wcel 1481   E.wrex 2418

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 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488

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

This theorem is referenced by:  rsp2e  2486  ssiun2  3864  tfrlem9  6224  tfrlemibxssdm  6232  tfr1onlembxssdm  6248  tfrcllembxssdm  6261  findcard2  6791  findcard2s  6792  prarloclemup  7327  prmuloc2  7399  ltaddpr  7429  aptiprlemu  7472  cauappcvgprlemopl  7478  cauappcvgprlemopu  7480  cauappcvgprlem2  7492  caucvgprlemopl  7501  caucvgprlemopu  7503  caucvgprlem2  7512  caucvgprprlem2  7542  suplocexprlemrl  7549  suplocexprlemru  7551  suplocexprlemlub  7556