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

Theorem rspec 2898
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 2894 . 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 1758   A.wral 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-ral 2804
This theorem is referenced by:  rspec2  2921  vtoclri  3153  isarep2  5609  ecopover  7317  alephsuc2  8365  indstr  11038  ackbijnn  13413  mrelatglb0  15478  0frgp  16401  frlmip  18338  iccpnfcnv  20658  rrxip  21036  wfis  27838  wfis2f  27840  wfis2  27842  frins  27874  frins2f  27876  prter2  29197
  Copyright terms: Public domain W3C validator