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
⊢ Ⅎ _ 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