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

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