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

Theorem hbxfrbi 1577
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2539 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 1575 . 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 1549
This theorem is referenced by:  hbe1w  1723  hbe1  1746  hba1  1804  hbanOLD  1851  hb3anOLD  1853  hbex  1863  hbab1  2425  hbab  2427  cleqh  2533  hbxfreq  2539  hbral  2754  hbra1  2755  hbra2VD  28972  bnj982  29149  bnj1095  29152  bnj1096  29153  bnj1276  29186  bnj594  29283  bnj1445  29413  hbexwAUX7  29449  hbexOLD7  29685
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator