Theorem hbxfrbi

A utility lemma to transfer a bound-variable hypothesis builder into a definition. See [hbxfreq] for equality version. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses
hbxfrbi.1
\( \vdash \varphi \leftrightarrow \psi \)
hbxfrbi.2
\( \vdash \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
Proof
l0
hbxfrbi.2
\( \vdash \psi \rightarrow \forall x \, \psi \)
l1
hbxfrbi.1
\( \vdash \varphi \leftrightarrow \psi \)
hbxfrbi.1
albii _
\( \vdash \forall x \, \varphi \leftrightarrow \forall x \, \psi \)
3imtr4i l0 l1 _