New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-un | Unicode version |
Description: Define the union of two classes. See elun 3220 for membership. (Contributed by SF, 10-Jan-2015.) |
Ref | Expression |
---|---|
df-un | ∼ &ncap ∼ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | cun 3207 | . 2 |
4 | 1 | ccompl 3205 | . . 3 ∼ |
5 | 2 | ccompl 3205 | . . 3 ∼ |
6 | 4, 5 | cnin 3204 | . 2 ∼ &ncap ∼ |
7 | 3, 6 | wceq 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 |