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

Theorem rspec 3115
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 3113 . 2 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
31, 2ax-mp 5 1 (𝑥𝐴𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  wral 3092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-12 2213
This theorem depends on definitions:  df-bi 198  df-ex 1860  df-ral 3097
This theorem is referenced by:  rspec2  3118  vtoclri  3472  wfis  5923  wfis2f  5925  wfis2  5927  isarep2  6183  ecopover  8081  alephsuc2  9180  indstr  11969  reltxrnmnf  12384  ackbijnn  14776  mrelatglb0  17384  0frgp  18387  iccpnfcnv  22950  frins  32061  frins2f  32063  prter2  34654
  Copyright terms: Public domain W3C validator