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

Theorem hbxfrbi 1824
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2871 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 1818 . 2 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
41, 2, 33imtr4i 292 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808
This theorem depends on definitions:  df-bi 207
This theorem is referenced by:  hbn1fw  2044  hbe1w  2047  hbe1  2142  hbsbwOLD  2171  hbab1OLD  2723  hbab  2724  hbabg  2725  hbxfreq  2871  hbral  3307  bnj982  34793  bnj1095  34796  bnj1096  34797  bnj1276  34829  bnj594  34927  bnj1445  35059  hbra2VD  44885
  Copyright terms: Public domain W3C validator