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

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

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2364 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 1446 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 119 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1287  wcel 1438  wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-4 1445
This theorem depends on definitions:  df-bi 115  df-ral 2364
This theorem is referenced by:  rsp2  2425  rspec  2427  r19.12  2478  ralbi  2501  rexbi  2502  reupick2  3285  dfiun2g  3762  iinss2  3782  invdisj  3839  mpteq12f  3918  trss  3945  sowlin  4147  reusv1  4280  reusv3  4282  ralxfrALT  4289  funimaexglem  5097  fun11iun  5274  fvmptssdm  5387  ffnfv  5456  riota5f  5632  mpt2eq123  5708  tfri3  6132  nneneq  6573  cauappcvgprlemladdru  7215  cauappcvgprlemladdrl  7216  caucvgprlemm  7227  indstr  9081  bezoutlemzz  11269  bj-rspgt  11686
  Copyright terms: Public domain W3C validator