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

Theorem rspec 2835
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 2833 . 2  |-  ( A. x  e.  A  ph  ->  ( x  e.  A  ->  ph ) )
31, 2ax-mp 5 1  |-  ( x  e.  A  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   A.wral 2817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-ral 2822
This theorem is referenced by:  rspec2  2839  vtoclri  3193  isarep2  5674  ecopover  7427  alephsuc2  8473  indstr  11162  ackbijnn  13620  mrelatglb0  15689  0frgp  16670  frlmip  18678  iccpnfcnv  21312  rrxip  21690  wfis  29217  wfis2f  29219  wfis2  29221  frins  29253  frins2f  29255  prter2  30550  fourierdlem62  31792
  Copyright terms: Public domain W3C validator