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

Theorem hbxfrbi 1822
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2870 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 1816 . 2 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
41, 2, 33imtr4i 292 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207
This theorem is referenced by:  hbn1fw  2043  hbe1w  2046  hbe1  2141  hbsbwOLD  2170  hbab1OLD  2722  hbab  2723  hbabg  2724  hbxfreq  2870  hbral  3306  bnj982  34771  bnj1095  34774  bnj1096  34775  bnj1276  34807  bnj594  34905  bnj1445  35037  hbra2VD  44858
  Copyright terms: Public domain W3C validator