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  6594  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  findcard2  7197  findcard2s  7198  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  16313