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

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

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2460 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 1511 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 121 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1351  wcel 2148  wral 2455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-4 1510
This theorem depends on definitions:  df-bi 117  df-ral 2460
This theorem is referenced by:  rspa  2525  rsp2  2527  rspec  2529  r19.12  2583  ralbi  2609  rexbi  2610  reupick2  3421  dfiun2g  3918  iinss2  3938  invdisj  3996  mpteq12f  4082  trss  4109  sowlin  4319  reusv1  4457  reusv3  4459  ralxfrALT  4466  funimaexglem  5298  fun11iun  5481  fvmptssdm  5599  ffnfv  5673  riota5f  5852  mpoeq123  5931  tfri3  6365  nneneq  6854  mkvprop  7153  cauappcvgprlemladdru  7652  cauappcvgprlemladdrl  7653  caucvgprlemm  7664  suplocexprlemss  7711  suplocsrlem  7804  indstr  9589  prodeq2  11558  fprodle  11641  bezoutlemzz  11995  sgrpidmndm  12753  srgdilem  13083  ringdilem  13126  tgcl  13435  fsumcncntop  13927  dedekindeulemlu  13970  dedekindicclemlu  13979  bj-rspgt  14398  bj-charfunr  14422
  Copyright terms: Public domain W3C validator