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 ⊢ A = B
hbxfr.2 ⊢ y ∈ B → ∀ x y ∈ B
Assertion hbxfreq ⊢ y ∈ A → ∀ x y ∈ A

Proof

Step Hyp Ref Expression
1 hbxfr.1 ⊢ A = B
2 hbxfr.2 ⊢ y ∈ B → ∀ x y ∈ B
3 1 eleq2i ⊢ y ∈ A ↔ y ∈ B
4 3 2 hbxfrbi ⊢ y ∈ A → ∀ x y ∈ A