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

Theorem rspec 2915
 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 2913 . 2 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
31, 2ax-mp 5 1 (𝑥𝐴𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1977  ∀wral 2896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-ex 1696  df-ral 2901 This theorem is referenced by:  rspec2  2918  vtoclri  3256  wfis  5633  wfis2f  5635  wfis2  5637  isarep2  5892  ecopover  7738  ecopoverOLD  7739  alephsuc2  8786  indstr  11632  reltxrnmnf  12043  ackbijnn  14399  mrelatglb0  17008  0frgp  18015  iccpnfcnv  22551  frins  30987  frins2f  30989  prter2  33184
 Copyright terms: Public domain W3C validator