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

Theorem rspec 2607
Description: Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
Hypothesis
Ref Expression
rspec.1  |-  A. x  e.  A  ph
Assertion
Ref Expression
rspec  |-  ( x  e.  A  ->  ph )

Proof of Theorem rspec
StepHypRef Expression
1 rspec.1 . 2  |-  A. x  e.  A  ph
2 rsp 2603 . 2  |-  ( A. x  e.  A  ph  ->  ( x  e.  A  ->  ph ) )
31, 2ax-mp 8 1  |-  ( x  e.  A  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   A.wral 2543
This theorem is referenced by:  rspec2  2642  vtoclri  2858  isarep2  5332  ecopover  6762  alephsuc2  7707  indstr  10287  ackbijnn  12286  mrelatglb0  14288  0frgp  15088  iccpnfcnv  18442  wfis  24210  wfis2f  24212  wfis2  24214  frins  24246  frins2f  24248  basexre  25522  intopcoaconlem3  25539  intopcoaconb  25540  intopcoaconc  25541  prter2  26749
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-ral 2548
  Copyright terms: Public domain W3C validator