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

Theorem rspec 3069
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 3067 . 2 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
31, 2ax-mp 5 1 (𝑥𝐴𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  wral 3050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196
This theorem depends on definitions:  df-bi 197  df-ex 1854  df-ral 3055
This theorem is referenced by:  rspec2  3072  vtoclri  3423  wfis  5877  wfis2f  5879  wfis2  5881  isarep2  6139  ecopover  8018  alephsuc2  9093  indstr  11949  reltxrnmnf  12365  ackbijnn  14759  mrelatglb0  17386  0frgp  18392  iccpnfcnv  22944  frins  32052  frins2f  32054  prter2  34670
  Copyright terms: Public domain W3C validator