Metamath Proof Explorer


Theorem nfab

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016) Add disjoint variable condition to avoid ax-13 . See nfabg for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024)

Ref Expression
Hypothesis nfab.1 x φ
Assertion nfab _ x y | φ

Proof

Step Hyp Ref Expression
1 nfab.1 x φ
2 1 nfsab x z y | φ
3 2 nfci _ x y | φ