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

Theorem rsp 2363
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 2305 . 2 (x A φx(x Aφ))
2 sp 1398 . 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 1240   wcel 1390  wral 2300
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-4 1397
This theorem depends on definitions:  df-bi 110  df-ral 2305
This theorem is referenced by:  rsp2  2365  rspec  2367  r19.12  2416  ralbi  2439  rexbi  2440  reupick2  3217  dfiun2g  3680  iinss2  3700  invdisj  3750  mpteq12f  3828  trss  3854  sowlin  4048  reusv1  4156  reusv3  4158  ralxfrALT  4165  funimaexglem  4925  fun11iun  5090  fvmptssdm  5198  ffnfv  5266  riota5f  5435  mpt2eq123  5506  tfri3  5894  indstr  8272  bj-rspgt  9194
  Copyright terms: Public domain W3C validator