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

Theorem hbxfrbi 1818
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2947 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 1813 . 2 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
41, 2, 33imtr4i 293 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 208
This theorem is referenced by:  hbn1fw  2045  hbe1w  2048  hbe1  2140  hbab1  2812  hbab  2815  hbabg  2816  hbxfreq  2947  hbral  3226  bnj982  31936  bnj1095  31939  bnj1096  31940  bnj1276  31972  bnj594  32070  bnj1445  32200  hbra2VD  41059
  Copyright terms: Public domain W3C validator