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  6595  tfrlemibxssdm  6603  tfr1onlembxssdm  6619  tfrcllembxssdm  6632  findcard2  7199  findcard2s  7200  prarloclemup  7868  prmuloc2  7940  ltaddpr  7970  aptiprlemu  8013  cauappcvgprlemopl  8019  cauappcvgprlemopu  8021  cauappcvgprlem2  8033  caucvgprlemopl  8042  caucvgprlemopu  8044  caucvgprlem2  8053  caucvgprprlem2  8083  suplocexprlemrl  8090  suplocexprlemru  8092  suplocexprlemlub  8097  bposlem3  16330