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

Theorem rspe 2772
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 1793 . 2  |-  ( ( x  e.  A  /\  ph )  ->  E. x
( x  e.  A  /\  ph ) )
2 df-rex 2716 . 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 1586    e. wcel 1756   E.wrex 2711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-rex 2716
This theorem is referenced by:  rsp2e  2774  2rmorex  3158  ssiun2  4208  reusv2lem3  4490  tfrlem9  6836  isinf  7518  findcard2  7544  findcard3  7547  scott0  8085  ac6c4  8642  supmul1  10287  supmul  10290  mreiincl  14526  restmetu  20137  bposlem3  22600  pjpjpre  24773  atom1d  25708  cvmlift2lem12  27155  supaddc  28370  supadd  28371  finminlem  28466  neibastop2lem  28534  prtlem18  28975  pell14qrdich  29163  2reurex  29958  bnj1398  31912
  Copyright terms: Public domain W3C validator