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 e. B -> A. x y e. B )
Assertion	hbxfreq	|- ( y e. A -> A. x y e. A )

Proof

Step	Hyp	Ref	Expression
1		hbxfr.1	|- A = B
2		hbxfr.2	|- ( y e. B -> A. x y e. B )
3	1	eleq2i	|- ( y e. A <-> y e. B )
4	3 2	hbxfrbi	|- ( y e. A -> A. x y e. A )