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

Theorem rspec 3204
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 3202 . 2 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
31, 2ax-mp 5 1 (𝑥𝐴𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-ex 1772  df-ral 3140
This theorem is referenced by:  rspec2  3208  vtoclri  3582  wfis  6177  wfis2f  6179  wfis2  6181  isarep2  6436  mpoexw  7765  ecopover  8390  alephsuc2  9494  indstr  12304  reltxrnmnf  12723  ackbijnn  15171  mrelatglb0  17783  0frgp  18834  iccpnfcnv  23475  frins  32985  frins2f  32987  prter2  35897
  Copyright terms: Public domain W3C validator