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

Theorem rspe 2604
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 1718 . 2  |-  ( ( x  e.  A  /\  ph )  ->  E. x
( x  e.  A  /\  ph ) )
2 df-rex 2549 . 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 1528    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  rsp2e  2606  2rmorex  2969  ssiun2  3945  reusv2lem3  4537  tfrlem9  6401  isinf  7076  findcard2  7098  findcard3  7100  scott0  7556  ac6c4  8108  supmul1  9719  supmul  9722  mreiincl  13498  bposlem3  20525  pjpjpre  21998  atom1d  22933  cvmlift2lem12  23845  finminlem  26231  neibastop2lem  26309  prtlem18  26745  pell14qrdich  26954  2reurex  27959  bnj1398  29064
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-ex 1529  df-rex 2549
  Copyright terms: Public domain W3C validator