Description: Disjoint union of two classes. This is a way of creating a set which contains elements corresponding to each element of A or B , tagging each one with whether it came from A or B . (Contributed by Jim Kingdon, 20-Jun-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | df-dju | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cA | |
|
1 | cB | |
|
2 | 0 1 | cdju | |
3 | c0 | |
|
4 | 3 | csn | |
5 | 4 0 | cxp | |
6 | c1o | |
|
7 | 6 | csn | |
8 | 7 1 | cxp | |
9 | 5 8 | cun | |
10 | 2 9 | wceq | |