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

Theorem rsp 2537
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 2473 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 sp 1522 . 2  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( x  e.  A  ->  ph ) )
31, 2sylbi 121 1  |-  ( A. x  e.  A  ph  ->  ( x  e.  A  ->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1362    e. wcel 2160   A.wral 2468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-4 1521
This theorem depends on definitions:  df-bi 117  df-ral 2473
This theorem is referenced by:  rspa  2538  rsp2  2540  rspec  2542  r19.12  2596  ralbi  2622  rexbi  2623  reupick2  3436  dfiun2g  3933  iinss2  3954  invdisj  4012  mpteq12f  4098  trss  4125  sowlin  4338  reusv1  4476  reusv3  4478  ralxfrALT  4485  funimaexglem  5318  fun11iun  5501  fvmptssdm  5620  ffnfv  5694  riota5f  5875  mpoeq123  5954  tfri3  6391  nneneq  6884  mkvprop  7185  cauappcvgprlemladdru  7684  cauappcvgprlemladdrl  7685  caucvgprlemm  7696  suplocexprlemss  7743  suplocsrlem  7836  indstr  9622  prodeq2  11596  fprodle  11679  bezoutlemzz  12034  sgrpidmndm  12878  srgdilem  13320  ringdilem  13363  tgcl  14016  fsumcncntop  14508  dedekindeulemlu  14551  dedekindicclemlu  14560  bj-rspgt  14991  bj-charfunr  15015
  Copyright terms: Public domain W3C validator