NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-in Unicode 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 &ncap

Detailed syntax breakdown of Definition df-in
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cin 3208 . 2
41, 2cnin 3204 . . 3 &ncap
54ccompl 3205 . 2 &ncap
63, 5wceq 1642 1 &ncap
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