Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The difference, union, and intersection of two classes
The difference of two classes
nfdif
Metamath Proof Explorer
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
|- F/_ x A
nfdif.2
|- F/_ x B
Assertion
nfdif
|- F/_ x ( A \ B )
Proof
Step
Hyp
Ref
Expression
1
nfdif.1
|- F/_ x A
2
nfdif.2
|- F/_ x B
3
eldif
|- ( y e. ( A \ B ) <-> ( y e. A /\ -. y e. B ) )
4
1
nfcri
|- F/ x y e. A
5
2
nfcri
|- F/ x y e. B
6
5
nfn
|- F/ x -. y e. B
7
4 6
nfan
|- F/ x ( y e. A /\ -. y e. B )
8
3 7
nfxfr
|- F/ x y e. ( A \ B )
9
8
nfci
|- F/_ x ( A \ B )