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

Theorem hbxfrbi 1826
 Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2881 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 1821 . 2 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
41, 2, 33imtr4i 295 1 (𝜑 → ∀𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210 This theorem is referenced by:  hbn1fw  2052  hbe1w  2055  hbe1  2144  hbsbw  2173  hbab1  2743  hbab  2746  hbabg  2747  hbxfreq  2881  hbral  3149  bnj982  32278  bnj1095  32281  bnj1096  32282  bnj1276  32314  bnj594  32412  bnj1445  32544  hbra2VD  41939
 Copyright terms: Public domain W3C validator