Metamath Proof Explorer


Theorem hbxfrbi

Description: 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)

Ref Expression
Hypotheses hbxfrbi.1 φ ψ
hbxfrbi.2 ψ x ψ
Assertion hbxfrbi φ x φ

Proof

Step Hyp Ref Expression
1 hbxfrbi.1 φ ψ
2 hbxfrbi.2 ψ x ψ
3 1 albii x φ x ψ
4 2 1 3 3imtr4i φ x φ