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

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

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2440 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 1491 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 120 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1333   ∈ wcel 2128  ∀wral 2435 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-4 1490 This theorem depends on definitions:  df-bi 116  df-ral 2440 This theorem is referenced by:  rspa  2505  rsp2  2507  rspec  2509  r19.12  2563  ralbi  2589  rexbi  2590  reupick2  3393  dfiun2g  3881  iinss2  3901  invdisj  3959  mpteq12f  4044  trss  4071  sowlin  4279  reusv1  4416  reusv3  4418  ralxfrALT  4425  funimaexglem  5250  fun11iun  5432  fvmptssdm  5549  ffnfv  5622  riota5f  5798  mpoeq123  5874  tfri3  6308  nneneq  6795  mkvprop  7084  cauappcvgprlemladdru  7559  cauappcvgprlemladdrl  7560  caucvgprlemm  7571  suplocexprlemss  7618  suplocsrlem  7711  indstr  9487  prodeq2  11436  fprodle  11519  bezoutlemzz  11866  tgcl  12424  fsumcncntop  12916  dedekindeulemlu  12959  dedekindicclemlu  12968  bj-rspgt  13319  bj-charfunr  13344
 Copyright terms: Public domain W3C validator