Theorem rspe 2922

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 1806	. 2 |- ( ( x e. A /\ ph ) -> E. x ( x e. A /\ ph ) )
2		df-rex 2820	. 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 369   E.wex 1596   e. wcel 1767   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803

This theorem depends on definitions:  df-bi 185  df-ex 1597  df-rex 2820

This theorem is referenced by:  rsp2e  2923  rsp2eOLD  2924  2rmorex  3308  ssiun2  4368  reusv2lem3  4650  tfrlem9  7051  isinf  7730  findcard2  7756  findcard3  7759  scott0  8300  ac6c4  8857  supmul1  10504  supmul  10507  mreiincl  14847  restmetu  20825  bposlem3  23289  pjpjpre  26013  atom1d  26948  cvmlift2lem12  28399  supaddc  29618  supadd  29619  finminlem  29713  neibastop2lem  29781  prtlem18  30222  pell14qrdich  30409  upbdrech  31082  limclner  31193  2reurex  31653  bnj1398  33169