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

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

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2311 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 1401 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 114 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1241   ∈ wcel 1393  ∀wral 2306 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-4 1400 This theorem depends on definitions:  df-bi 110  df-ral 2311 This theorem is referenced by:  rsp2  2371  rspec  2373  r19.12  2422  ralbi  2445  rexbi  2446  reupick2  3223  dfiun2g  3689  iinss2  3709  invdisj  3759  mpteq12f  3837  trss  3863  sowlin  4057  reusv1  4190  reusv3  4192  ralxfrALT  4199  funimaexglem  4982  fun11iun  5147  fvmptssdm  5255  ffnfv  5323  riota5f  5492  mpt2eq123  5564  tfri3  5953  nneneq  6320  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemm  6766  indstr  8536  bj-rspgt  9925
 Copyright terms: Public domain W3C validator