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

Theorem hbxfrbi 1402
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 1400 . 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 1283
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 1377  ax-gen 1379
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  hbbi  1481  hb3or  1482  hb3an  1483  hbs1f  1705  hbs1  1856  hbsbv  1859  hbeu1  1952  sb8euh  1965  hbmo1  1980  hbmo  1981  hbab1  2071  hbab  2073  cleqh  2179  hbxfreq  2186  hbral  2396  hbra1  2397
  Copyright terms: Public domain W3C validator