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

Theorem hbxfrbi 1429
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 1427 . 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 1310
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  hbbi  1508  hb3or  1509  hb3an  1510  hbs1f  1735  hbs1  1887  hbsbv  1890  hbeu1  1983  sb8euh  1996  hbmo1  2011  hbmo  2012  hbab1  2102  hbab  2104  cleqh  2212  hbxfreq  2219  hbral  2436  hbra1  2437
  Copyright terms: Public domain W3C validator