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

Theorem rspe 2893
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 1797 . 2  |-  ( ( x  e.  A  /\  ph )  ->  E. x
( x  e.  A  /\  ph ) )
2 df-rex 2804 . 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 1587    e. wcel 1758   E.wrex 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-rex 2804
This theorem is referenced by:  rsp2e  2895  2rmorex  3269  ssiun2  4320  reusv2lem3  4602  tfrlem9  6953  isinf  7636  findcard2  7662  findcard3  7665  scott0  8203  ac6c4  8760  supmul1  10405  supmul  10408  mreiincl  14652  restmetu  20293  bposlem3  22757  pjpjpre  24973  atom1d  25908  cvmlift2lem12  27346  supaddc  28564  supadd  28565  finminlem  28660  neibastop2lem  28728  prtlem18  29169  pell14qrdich  29357  2reurex  30152  bnj1398  32342
  Copyright terms: Public domain W3C validator