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

Theorem hbxfrbi 1828
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2869 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 1822 . 2 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
41, 2, 33imtr4i 292 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206
This theorem is referenced by:  hbn1fw  2049  hbe1w  2052  hbe1  2140  hbsbw  2170  hbab1OLD  2724  hbab  2725  hbabg  2726  hbxfreq  2869  hbral  3294  bnj982  33430  bnj1095  33433  bnj1096  33434  bnj1276  33466  bnj594  33564  bnj1445  33696  hbra2VD  43216
  Copyright terms: Public domain W3C validator