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

Theorem rspec 2713
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 2709 . 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 1717   A.wral 2649
This theorem is referenced by:  rspec2  2748  vtoclri  2969  isarep2  5473  ecopover  6944  alephsuc2  7894  indstr  10477  ackbijnn  12534  mrelatglb0  14538  0frgp  15338  iccpnfcnv  18840  wfis  25234  wfis2f  25236  wfis2  25238  frins  25270  frins2f  25272  prter2  26421
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-ral 2654
  Copyright terms: Public domain W3C validator