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

Metamath Proof Explorer

Theorem nfsab1

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016) Remove use of ax-12 . (Revised by SN, 20-Sep-2023)

Ref Expression
Assertion nfsab1 ⊢ Ⅎ x y ∈ x | φ

Proof

Step Hyp Ref Expression
1 df-clab ⊢ y ∈ x | φ ↔ y x φ
2 nfs1v ⊢ Ⅎ x y x φ
3 1 2 nfxfr ⊢ Ⅎ x y ∈ x | φ