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

Metamath Proof Explorer

Theorem bj-nfsab1

Description: Remove dependency on ax-13 from nfsab1 . UPDATE / TODO: nfsab1 does not use ax-13 either anymore; bj-nfsab1 is shorter than nfsab1 but uses ax-12 . (Contributed by BJ, 23-Jun-2019) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hbab1 ⊢ y ∈ x | φ → ∀ x y ∈ x | φ
2 1 nf5i ⊢ Ⅎ x y ∈ x | φ