Metamath Proof Explorer


Theorem nfaba1

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016) Add disjoint variable condition to avoid ax-13 . See nfaba1g for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024) Avoid ax-6 , ax-7 , ax-12 . (Revised by SN, 14-May-2025)

Ref Expression
Assertion nfaba1 _ x y | x φ

Proof

Step Hyp Ref Expression
1 df-clab z y | x φ z y x φ
2 sbal z y x φ x z y φ
3 nfa1 x x z y φ
4 2 3 nfxfr x z y x φ
5 1 4 nfxfr x z y | x φ
6 5 nfci _ x y | x φ