df-dif - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > df-dif		Unicode version

Definition df-dif 3215

Description: Define the difference of two classes. See eldif 3221 for membership. (Contributed by SF, 10-Jan-2015.)

**Assertion**
Ref	Expression
df-dif	∼

**Detailed syntax breakdown of Definition df-dif**
Step	Hyp	Ref	Expression
1		cA	. . 3
2		cB	. . 3
3	1, 2	cdif 3206	. 2
4	2	ccompl 3205	. . 3 ∼
5	1, 4	cin 3208	. 2 ∼
6	3, 5	wceq 1642	1 ∼

Colors of variables: wff setvar class

This definition is referenced by: eldif 3221 nfdif 3232 difeq1 3246 difeq2 3247 difsscompl 3549 compldif 4069 inindif 4075 difexg 4102 nnsucelrlem3 4426 ssfin 4470 sbthlem1 6203