Theorem rspe 2727

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

Syntax hints:   -> wi 4   /\ wa 359   E.wex 1547   e. wcel 1721   E.wrex 2667

This theorem is referenced by:  rsp2e  2729  2rmorex  3098  ssiun2  4094  reusv2lem3  4685  tfrlem9  6605  isinf  7281  findcard2  7307  findcard3  7309  scott0  7766  ac6c4  8317  supmul1  9929  supmul  9932  mreiincl  13776  restmetu  18570  bposlem3  21023  pjpjpre  22874  atom1d  23809  cvmlift2lem12  24954  supaddc  26137  supadd  26138  finminlem  26211  neibastop2lem  26279  prtlem18  26616  pell14qrdich  26822  2reurex  27826  bnj1398  29109

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-rex 2672