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

Theorem hbxfrbi 1433
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
hbxfrbi.1  |-  ( ph  <->  ps )
hbxfrbi.2  |-  ( ps 
->  A. x ps )
Assertion
Ref Expression
hbxfrbi  |-  ( ph  ->  A. x ph )

Proof of Theorem hbxfrbi
StepHypRef Expression
1 hbxfrbi.2 . 2  |-  ( ps 
->  A. x ps )
2 hbxfrbi.1 . 2  |-  ( ph  <->  ps )
32albii 1431 . 2  |-  ( A. x ph  <->  A. x ps )
41, 2, 33imtr4i 200 1  |-  ( ph  ->  A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   A.wal 1314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  hbbi  1512  hb3or  1513  hb3an  1514  hbs1f  1739  hbs1  1891  hbsbv  1894  hbeu1  1987  sb8euh  2000  hbmo1  2015  hbmo  2016  hbab1  2106  hbab  2108  cleqh  2217  hbxfreq  2224  hbral  2441  hbra1  2442
  Copyright terms: Public domain W3C validator