Metamath Proof Explorer


Theorem nfdif

Description: Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003) (Revised by Mario Carneiro, 13-Oct-2016) Avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 14-May-2025)

Ref Expression
Hypotheses nfdif.1 _ x A
nfdif.2 _ x B
Assertion nfdif _ x A B

Proof

Step Hyp Ref Expression
1 nfdif.1 _ x A
2 nfdif.2 _ x B
3 eldif y A B y A ¬ y B
4 1 nfcri x y A
5 2 nfcri x y B
6 5 nfn x ¬ y B
7 4 6 nfan x y A ¬ y B
8 3 7 nfxfr x y A B
9 8 nfci _ x A B