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

Definition df-in 3213
Description: Define the intersection of two classes. See elin 3219 for membership. (Contributed by SF, 10-Jan-2015.)
Assertion
Ref Expression
df-in (AB) = ∼ (AB)

Detailed syntax breakdown of Definition df-in
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cin 3208 . 2 class (AB)
41, 2cnin 3204 . . 3 class (AB)
54ccompl 3205 . 2 class ∼ (AB)
63, 5wceq 1642 1 wff (AB) = ∼ (AB)
Colors of variables: wff setvar class
This definition is referenced by:  elin  3219  nfin  3230  difeq1  3246  difeq2  3247  dfin5  3545  incompl  4073  inexg  4100
  Copyright terms: Public domain W3C validator