MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hbxfrbi Unicode version

Theorem hbxfrbi 1568
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2461 for equality version. (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 1566 . 2  |-  ( A. x ph  <->  A. x ps )
41, 2, 33imtr4i 257 1  |-  ( ph  ->  A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1540
This theorem is referenced by:  hbe1w  1708  hbe1  1731  hbanOLD  1834  hb3anOLD  1836  hbex  1846  hbab1  2347  hbab  2349  cleqh  2455  hbxfreq  2461  hbral  2667  hbra1  2668  hbra2VD  28381  bnj982  28555  bnj1095  28558  bnj1096  28559  bnj1276  28592  bnj594  28689  hbexwAUX7  28855  hbexOLD7  29069  ax9lem10  29201
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator