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

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

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2328 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 1417 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 118 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1257  wcel 1409  wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-4 1416
This theorem depends on definitions:  df-bi 114  df-ral 2328
This theorem is referenced by:  rsp2  2388  rspec  2390  r19.12  2439  ralbi  2462  rexbi  2463  reupick2  3251  dfiun2g  3717  iinss2  3737  invdisj  3787  mpteq12f  3865  trss  3891  sowlin  4085  reusv1  4218  reusv3  4220  ralxfrALT  4227  funimaexglem  5010  fun11iun  5175  fvmptssdm  5283  ffnfv  5351  riota5f  5520  mpt2eq123  5592  tfri3  5984  nneneq  6351  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgprlemm  6824  indstr  8632  bj-rspgt  10312
  Copyright terms: Public domain W3C validator