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

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

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2488 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 1533 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 121 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1370  wcel 2175  wral 2483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-4 1532
This theorem depends on definitions:  df-bi 117  df-ral 2488
This theorem is referenced by:  rspa  2553  rsp2  2555  rspec  2557  r19.12  2611  ralbi  2637  rexbi  2638  reupick2  3458  dfiun2g  3958  iinss2  3979  invdisj  4037  mpteq12f  4123  trss  4150  sowlin  4366  reusv1  4504  reusv3  4506  ralxfrALT  4513  funimaexglem  5356  fun11iun  5542  fvmptssdm  5663  ffnfv  5737  riota5f  5923  mpoeq123  6003  tfri3  6452  nneneq  6953  mkvprop  7259  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgprlemm  7780  suplocexprlemss  7827  suplocsrlem  7920  indstr  9713  nninfinf  10586  prodeq2  11810  fprodle  11893  bezoutlemzz  12265  sgrpidmndm  13194  srgdilem  13673  ringdilem  13716  tgcl  14478  fsumcncntop  14981  dedekindeulemlu  15035  dedekindicclemlu  15044  bj-rspgt  15655  bj-charfunr  15679
  Copyright terms: Public domain W3C validator