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

Detailed syntax breakdown of Definition df-un
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cun 3207 . 2 class (AB)
41ccompl 3205 . . 3 class A
52ccompl 3205 . . 3 class B
64, 5cnin 3204 . 2 class ( ∼ A ⩃ ∼ B)
73, 6wceq 1642 1 wff (AB) = ( ∼ A ⩃ ∼ B)
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