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 2865 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  2720  hbab  2721  hbabg  2722  hbxfreq  2865  hbral  3306  bnj982  33720  bnj1095  33723  bnj1096  33724  bnj1276  33756  bnj594  33854  bnj1445  33986  hbra2VD  43492
  Copyright terms: Public domain W3C validator