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

Theorem rsp 2439
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 2380 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 sp 1456 . 2  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( x  e.  A  ->  ph ) )
31, 2sylbi 120 1  |-  ( A. x  e.  A  ph  ->  ( x  e.  A  ->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1297    e. wcel 1448   A.wral 2375
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-4 1455
This theorem depends on definitions:  df-bi 116  df-ral 2380
This theorem is referenced by:  rsp2  2441  rspec  2443  r19.12  2497  ralbi  2523  rexbi  2524  reupick2  3309  dfiun2g  3792  iinss2  3812  invdisj  3869  mpteq12f  3948  trss  3975  sowlin  4180  reusv1  4317  reusv3  4319  ralxfrALT  4326  funimaexglem  5142  fun11iun  5322  fvmptssdm  5437  ffnfv  5510  riota5f  5686  mpoeq123  5762  tfri3  6194  nneneq  6680  mkvprop  6943  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  caucvgprlemm  7377  indstr  9238  bezoutlemzz  11483  tgcl  12015  bj-rspgt  12574
  Copyright terms: Public domain W3C validator