This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )