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

Theorem hbxfrbi 1482
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 1480 . 2  |-  ( A. x ph  <->  A. x ps )
41, 2, 33imtr4i 201 1  |-  ( ph  ->  A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   A.wal 1361
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  hbbi  1558  hb3or  1559  hb3an  1560  hbs1f  1791  hbs1  1949  hbsbv  1952  hbeu1  2047  sb8euh  2060  hbmo1  2075  hbmo  2076  hbab1  2177  hbab  2179  cleqh  2288  hbxfreq  2295  hbral  2518  hbra1  2519
  Copyright terms: Public domain W3C validator