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

Theorem hbxfrbi 1555
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2386 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 1553 . 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 1527
This theorem is referenced by:  hbe1w  1682  hbe1  1705  hbex  1733  hban  1736  hb3an  1759  hbab1  2272  hbab  2274  cleqh  2380  hbxfreq  2386  hbral  2591  hbra1  2592  hbra2VD  28636  bnj982  28810  bnj1095  28813  bnj1096  28814  bnj1276  28847  bnj594  28944  ax9lem10  29149
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator