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

Theorem hbxfrbi 1827
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2864 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 291 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1539
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 206
This theorem is referenced by:  hbn1fw  2048  hbe1w  2051  hbe1  2139  hbsbw  2169  hbab1OLD  2719  hbab  2720  hbabg  2721  hbxfreq  2864  hbral  3305  bnj982  33858  bnj1095  33861  bnj1096  33862  bnj1276  33894  bnj594  33992  bnj1445  34124  hbra2VD  43703
  Copyright terms: Public domain W3C validator