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

Definition df-un 3214
Description: Define the union of two classes. See elun 3220 for membership. (Contributed by SF, 10-Jan-2015.)
Assertion
Ref Expression
df-un &ncap ∼

Detailed syntax breakdown of Definition df-un
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cun 3207 . 2
41ccompl 3205 . . 3
52ccompl 3205 . . 3
64, 5cnin 3204 . 2 &ncap ∼
73, 6wceq 1642 1 &ncap ∼
Colors of variables: wff setvar class
This definition is referenced by:  elun  3220  nfun  3231  symdifeq1  3248  symdifeq2  3249  dfin5  3545  uncompl  4074  unexg  4101
  Copyright terms: Public domain W3C validator