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

Theorem rspe 2915
Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.)
Assertion
Ref Expression
rspe

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 1857 . 2
2 df-rex 2813 . 2
31, 2sylibr 212 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  E.wex 1612  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  rsp2e  2916  rsp2eOLD  2917  2rmorex  3304  ssiun2  4373  reusv2lem3  4655  tfrlem9  7073  isinf  7753  findcard2  7780  findcard3  7783  scott0  8325  ac6c4  8882  supmul1  10533  supmul  10536  mreiincl  14993  restmetu  21090  bposlem3  23561  opphllem5  24123  pjpjpre  26337  atom1d  27272  cvmlift2lem12  28759  supaddc  30041  supadd  30042  finminlem  30136  neibastop2lem  30178  prtlem18  30618  pell14qrdich  30805  upbdrech  31505  limclner  31657  2reurex  32186  bnj1398  34090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-rex 2813
  Copyright terms: Public domain W3C validator