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

Theorem rsp 2423
Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.)
Assertion
Ref Expression
rsp  |-  ( A. x  e.  A  ph  ->  ( x  e.  A  ->  ph ) )

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2364 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 sp 1446 . 2  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( x  e.  A  ->  ph ) )
31, 2sylbi 119 1  |-  ( A. x  e.  A  ph  ->  ( x  e.  A  ->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1287    e. wcel 1438   A.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  3283  dfiun2g  3757  iinss2  3777  invdisj  3831  mpteq12f  3910  trss  3937  sowlin  4138  reusv1  4271  reusv3  4273  ralxfrALT  4280  funimaexglem  5083  fun11iun  5258  fvmptssdm  5371  ffnfv  5440  riota5f  5614  mpt2eq123  5690  tfri3  6114  nneneq  6553  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  caucvgprlemm  7206  indstr  9050  bezoutlemzz  11073  bj-rspgt  11332
  Copyright terms: Public domain W3C validator