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

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

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2396 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 1471 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 120 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1312  wcel 1463  wral 2391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-4 1470
This theorem depends on definitions:  df-bi 116  df-ral 2396
This theorem is referenced by:  rsp2  2457  rspec  2459  r19.12  2513  ralbi  2539  rexbi  2540  reupick2  3330  dfiun2g  3813  iinss2  3833  invdisj  3891  mpteq12f  3976  trss  4003  sowlin  4210  reusv1  4347  reusv3  4349  ralxfrALT  4356  funimaexglem  5174  fun11iun  5354  fvmptssdm  5471  ffnfv  5544  riota5f  5720  mpoeq123  5796  tfri3  6230  nneneq  6717  mkvprop  6998  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  caucvgprlemm  7440  suplocexprlemss  7487  suplocsrlem  7580  indstr  9340  bezoutlemzz  11597  tgcl  12139  fsumcncntop  12631  dedekindeulemlu  12674  dedekindicclemlu  12683  bj-rspgt  12827
  Copyright terms: Public domain W3C validator