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

Theorem rspe 2680
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 1747 . 2  |-  ( ( x  e.  A  /\  ph )  ->  E. x
( x  e.  A  /\  ph ) )
2 df-rex 2625 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
31, 2sylibr 203 1  |-  ( ( x  e.  A  /\  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1541    e. wcel 1710   E.wrex 2620
This theorem is referenced by:  rsp2e  2682  2rmorex  3045  ssiun2  4024  reusv2lem3  4616  tfrlem9  6485  isinf  7161  findcard2  7185  findcard3  7187  scott0  7643  ac6c4  8195  supmul1  9806  supmul  9809  mreiincl  13591  bposlem3  20631  pjpjpre  22106  atom1d  23041  restmetu  23615  cvmlift2lem12  24249  supaddc  25482  supadd  25483  finminlem  25555  neibastop2lem  25633  prtlem18  26068  pell14qrdich  26277  2reurex  27282  bnj1398  28809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-rex 2625
  Copyright terms: Public domain W3C validator