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

Theorem rspe 2731
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 2676 . 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 2671
This theorem is referenced by:  rsp2e  2733  2rmorex  3102  ssiun2  4098  reusv2lem3  4689  tfrlem9  6609  isinf  7285  findcard2  7311  findcard3  7313  scott0  7770  ac6c4  8321  supmul1  9933  supmul  9936  mreiincl  13780  restmetu  18574  bposlem3  21027  pjpjpre  22878  atom1d  23813  cvmlift2lem12  24958  supaddc  26141  supadd  26142  finminlem  26215  neibastop2lem  26283  prtlem18  26620  pell14qrdich  26826  2reurex  27830  bnj1398  29113
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 2676
  Copyright terms: Public domain W3C validator