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

Theorem rsp 2347
Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.)
Assertion
Ref Expression
rsp (x A φ → (x Aφ))

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2289 . 2 (x A φx(x Aφ))
2 sp 1382 . 2 (x(x Aφ) → (x Aφ))
31, 2sylbi 114 1 (x A φ → (x Aφ))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1226   wcel 1374  wral 2284
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-4 1381
This theorem depends on definitions:  df-bi 110  df-ral 2289
This theorem is referenced by:  rsp2  2349  rspec  2351  r19.12  2400  ralbi  2423  rexbi  2424  reupick2  3200  dfiun2g  3663  iinss2  3683  invdisj  3733  mpteq12f  3811  trss  3837  sowlin  4031  reusv1  4140  reusv3  4142  ralxfrALT  4149  funimaexglem  4908  fun11iun  5072  fvmptssdm  5180  ffnfv  5248  riota5f  5416  mpt2eq123  5487  tfri3  5875  bj-rspgt  7032
  Copyright terms: Public domain W3C validator