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

Theorem rspe 2844
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 1955 . 2  |-  ( ( x  e.  A  /\  ph )  ->  E. x
( x  e.  A  /\  ph ) )
2 df-rex 2762 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
31, 2sylibr 217 1  |-  ( ( x  e.  A  /\  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376   E.wex 1671    e. wcel 1904   E.wrex 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950
This theorem depends on definitions:  df-bi 190  df-ex 1672  df-rex 2762
This theorem is referenced by:  rsp2e  2845  2rmorex  3232  ssiun2  4312  reusv2lem3  4604  tfrlem9  7121  isinf  7803  findcard2  7829  findcard3  7832  scott0  8375  ac6c4  8929  supaddc  10596  supadd  10597  supmul1  10598  supmul  10601  mreiincl  15580  restmetu  21663  bposlem3  24293  opphllem5  24872  pjpjpre  27153  atom1d  28087  bnj1398  29915  cvmlift2lem12  30109  finminlem  31045  neibastop2lem  31087  iooelexlt  31835  relowlpssretop  31837  prtlem18  32513  pell14qrdich  35786  disjinfi  37539  iunmapsn  37570  upbdrech  37611  limclner  37829  sge0iunmptlemre  38371  iundjiun  38414  isomenndlem  38470  ovnsubaddlem1  38510  2reurex  38747
  Copyright terms: Public domain W3C validator