ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rsp GIF version

Theorem rsp 2457
Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.)
Assertion
Ref Expression
rsp (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2398 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 1473 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 120 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1314  wcel 1465  wral 2393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-4 1472
This theorem depends on definitions:  df-bi 116  df-ral 2398
This theorem is referenced by:  rsp2  2459  rspec  2461  r19.12  2515  ralbi  2541  rexbi  2542  reupick2  3332  dfiun2g  3815  iinss2  3835  invdisj  3893  mpteq12f  3978  trss  4005  sowlin  4212  reusv1  4349  reusv3  4351  ralxfrALT  4358  funimaexglem  5176  fun11iun  5356  fvmptssdm  5473  ffnfv  5546  riota5f  5722  mpoeq123  5798  tfri3  6232  nneneq  6719  mkvprop  7000  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  caucvgprlemm  7444  suplocexprlemss  7491  suplocsrlem  7584  indstr  9356  bezoutlemzz  11617  tgcl  12160  fsumcncntop  12652  dedekindeulemlu  12695  dedekindicclemlu  12704  bj-rspgt  12920
  Copyright terms: Public domain W3C validator