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

Theorem hbxfrbi 1404
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 1402 . 2  |-  ( A. x ph  <->  A. x ps )
41, 2, 33imtr4i 199 1  |-  ( ph  ->  A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   A.wal 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  hbbi  1483  hb3or  1484  hb3an  1485  hbs1f  1708  hbs1  1859  hbsbv  1862  hbeu1  1955  sb8euh  1968  hbmo1  1983  hbmo  1984  hbab1  2074  hbab  2076  cleqh  2184  hbxfreq  2191  hbral  2403  hbra1  2404
  Copyright terms: Public domain W3C validator