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

Metamath Proof Explorer

Theorem hbab1

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 26-May-1993) (Proof shortened by Wolf Lammen, 25-Oct-2024)

Ref Expression
Assertion hbab1 ⊢ y ∈ x | φ → ∀ x y ∈ x | φ

Proof

Step Hyp Ref Expression
1 nfsab1 ⊢ Ⅎ x y ∈ x | φ
2 1 nf5ri ⊢ y ∈ x | φ → ∀ x y ∈ x | φ