MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspe Unicode version

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
StepHypRef 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 )
)
31, 2sylibr 204 1  |-  ( ( x  e.  A  /\  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator