Nearby theorems
|
|
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > NFE Home > Th. List > df-uni | Unicode version | ||
Description: Define the union of a
class i.e. the collection of all members of the
members of the class. Definition 5.5 of [TakeutiZaring] p. 16. For
example,   1 , 3   1 , 8  1 , 3 , 8
(ex-uni in set.mm). This is similar to the union of two classes
df-un 3214. (Contributed by NM,
23-Aug-1993.) |
| Ref | Expression |
|---|---|
| df-uni |
        "){kind=small} |
,,| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
 | |
| 2 | 1 | cuni 3891 |
. 2
|
| 3 | vx |
. . . . . 6
 | |
| 4 | vy |
. . . . . 6
| |
| 5 | 3, 4 | wel 1711 |
. . . . 5
 |
| 6 | 4 | cv 1641 |
. . . . . 6
|
| 7 | 6, 1 | wcel 1710 |
. . . . 5
|
| 8 | 5, 7 | wa 358 |
. . . 4
|
| 9 | 8, 4 | wex 1541 |
. . 3
|
| 10 | 9, 3 | cab 2339 |
. 2
|
| 11 | 2, 10 | wceq 1642 |
1
|
| Colors of variables: wff setvar class |
| This definition is referenced by: dfuni2 3893 eluni 3894 csbunig 3899 |
| Copyright terms: Public domain | W3C validator |