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

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