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

Theorem rspec 2620
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 2616 . 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 1696   A.wral 2556
This theorem is referenced by:  rspec2  2655  vtoclri  2871  isarep2  5348  ecopover  6778  alephsuc2  7723  indstr  10303  ackbijnn  12302  mrelatglb0  14304  0frgp  15104  iccpnfcnv  18458  wfis  24281  wfis2f  24283  wfis2  24285  frins  24317  frins2f  24319  basexre  25625  intopcoaconlem3  25642  intopcoaconb  25643  intopcoaconc  25644  prter2  26852
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-ral 2561
  Copyright terms: Public domain W3C validator