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

Theorem rspec 3247
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 3244 . 2 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
31, 2ax-mp 5 1 (𝑥𝐴𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-ex 1782  df-ral 3062
This theorem is referenced by:  rspec2  3276  vtoclri  3576  wfis  6353  wfis2f  6356  wfis2  6358  isarep2  6636  mpoexw  8061  ecopover  8811  frins  9743  alephsuc2  10071  indstr  12896  reltxrnmnf  13317  ackbijnn  15770  mrelatglb0  18510  0frgp  19641  iccpnfcnv  24451  prter2  37739  natlocalincr  45576  natglobalincr  45577
  Copyright terms: Public domain W3C validator