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

Theorem rspec 3157
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 3155 . 2 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
31, 2ax-mp 5 1 (𝑥𝐴𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2050  wral 3088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-12 2106
This theorem depends on definitions:  df-bi 199  df-ex 1743  df-ral 3093
This theorem is referenced by:  rspec2  3161  vtoclri  3504  wfis  6024  wfis2f  6026  wfis2  6028  isarep2  6278  mpoexw  7586  ecopover  8203  alephsuc2  9302  indstr  12133  reltxrnmnf  12554  ackbijnn  15046  mrelatglb0  17656  0frgp  18668  iccpnfcnv  23254  frins  32609  frins2f  32611  prter2  35462
  Copyright terms: Public domain W3C validator