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

Theorem hbxfrbi 1643
 Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2579 for equality version. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
hbxfrbi.1
hbxfrbi.2
Assertion
Ref Expression
hbxfrbi

Proof of Theorem hbxfrbi
StepHypRef Expression
1 hbxfrbi.2 . 2
2 hbxfrbi.1 . 2
32albii 1640 . 2
41, 2, 33imtr4i 266 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  A.wal 1393 This theorem is referenced by:  hbn1fw  1812  hbe1w  1815  hbe1  1839  hba1  1896  hbex  1946  hbab1  2445  hbab  2447  cleqhOLD  2573  hbxfreq  2579  hbra1OLD  2840  hbral  2841  hbra2VD  33660  bnj982  33837  bnj1095  33840  bnj1096  33841  bnj1276  33873  bnj594  33970  bnj1445  34100  bj-hbab1  34356  bj-cleqh  34358 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631 This theorem depends on definitions:  df-bi 185
 Copyright terms: Public domain W3C validator