Theorem rspe 2861

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

Syntax hints:   -> wi 4   /\ wa 367   E.wex 1633   e. wcel 1842   E.wrex 2754

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-12 1878

This theorem depends on definitions:  df-bi 185  df-ex 1634  df-rex 2759

This theorem is referenced by:  rsp2e  2862  rsp2eOLD  2863  2rmorex  3253  ssiun2  4313  reusv2lem3  4596  tfrlem9  7087  isinf  7767  findcard2  7793  findcard3  7796  scott0  8335  ac6c4  8892  supmul1  10547  supmul  10550  mreiincl  15208  restmetu  21380  bposlem3  23940  opphllem5  24506  pjpjpre  26737  atom1d  27671  bnj1398  29404  cvmlift2lem12  29598  finminlem  30533  neibastop2lem  30575  supaddc  31393  supadd  31394  prtlem18  31880  pell14qrdich  35146  upbdrech  36854  limclner  37006  2reurex  37535