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

Theorem rspe 2773
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 1764 . 2  |-  ( ( x  e.  A  /\  ph )  ->  E. x
( x  e.  A  /\  ph ) )
2 df-rex 2717 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
31, 2sylibr 205 1  |-  ( ( x  e.  A  /\  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   E.wex 1551    e. wcel 1727   E.wrex 2712
This theorem is referenced by:  rsp2e  2775  2rmorex  3144  ssiun2  4158  reusv2lem3  4755  tfrlem9  6675  isinf  7351  findcard2  7377  findcard3  7379  scott0  7841  ac6c4  8392  supmul1  10004  supmul  10007  mreiincl  13852  restmetu  18648  bposlem3  21101  pjpjpre  22952  atom1d  23887  cvmlift2lem12  25032  supaddc  26269  supadd  26270  finminlem  26359  neibastop2lem  26427  prtlem18  26764  pell14qrdich  26970  2reurex  27973  bnj1398  29501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-11 1763
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-rex 2717
  Copyright terms: Public domain W3C validator