Metamath Proof Explorer


Theorem hbxfreq

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi for equivalence version. (Contributed by NM, 21-Aug-2007)

Ref Expression
Hypotheses hbxfr.1 𝐴 = 𝐵
hbxfr.2 ( 𝑦𝐵 → ∀ 𝑥 𝑦𝐵 )
Assertion hbxfreq ( 𝑦𝐴 → ∀ 𝑥 𝑦𝐴 )

Proof

Step Hyp Ref Expression
1 hbxfr.1 𝐴 = 𝐵
2 hbxfr.2 ( 𝑦𝐵 → ∀ 𝑥 𝑦𝐵 )
3 1 eleq2i ( 𝑦𝐴𝑦𝐵 )
4 3 2 hbxfrbi ( 𝑦𝐴 → ∀ 𝑥 𝑦𝐴 )