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

Theorem hbxfrbi 1574
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2507 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 1572 . 2  |-  ( A. x ph  <->  A. x ps )
41, 2, 33imtr4i 258 1  |-  ( ph  ->  A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546
This theorem is referenced by:  hbe1w  1719  hbe1  1742  hba1  1800  hbanOLD  1847  hb3anOLD  1849  hbex  1859  hbab1  2393  hbab  2395  cleqh  2501  hbxfreq  2507  hbral  2714  hbra1  2715  hbra2VD  28681  bnj982  28855  bnj1095  28858  bnj1096  28859  bnj1276  28892  bnj594  28989  bnj1445  29119  hbexwAUX7  29155  hbexOLD7  29369
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator