NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-dif GIF 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 (A B) = (A ∩ ∼ B)

Detailed syntax breakdown of Definition df-dif
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cdif 3206 . 2 class (A B)
42ccompl 3205 . . 3 class B
51, 4cin 3208 . 2 class (A ∩ ∼ B)
63, 5wceq 1642 1 wff (A B) = (A ∩ ∼ B)
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
  Copyright terms: Public domain W3C validator