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	$$⊢A=B$$
	hbxfr.2	$$⊢y\in B\to \forall xy\in B$$
Assertion	hbxfreq	$$⊢y\in A\to \forall xy\in A$$

Proof

Step	Hyp	Ref	Expression
1		hbxfr.1	$$⊢A=B$$
2		hbxfr.2	$$⊢y\in B\to \forall xy\in B$$
3	1	eleq2i	$$⊢y\in A\leftrightarrow y\in B$$
4	3 2	hbxfrbi	$$⊢y\in A\to \forall xy\in A$$