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

Theorem rspec 2762
 Description: Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
Hypothesis
Ref Expression
rspec.1
Assertion
Ref Expression
rspec

Proof of Theorem rspec
StepHypRef Expression
1 rspec.1 . 2
2 rsp 2758 . 2
31, 2ax-mp 8 1
 Colors of variables: wff set class Syntax hints:   wi 4   wcel 1725  wral 2697 This theorem is referenced by:  rspec2  2797  vtoclri  3018  isarep2  5525  ecopover  7000  alephsuc2  7953  indstr  10537  ackbijnn  12599  mrelatglb0  14603  0frgp  15403  iccpnfcnv  18961  wfis  25477  wfis2f  25479  wfis2  25481  frins  25513  frins2f  25515  prter2  26721 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761 This theorem depends on definitions:  df-bi 178  df-ex 1551  df-ral 2702
 Copyright terms: Public domain W3C validator