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 | |- ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | |- A |
|
| 1 | cB | |- B |
|
| 2 | 0 1 | cdju | |- ( A |_| B ) |
| 3 | c0 | |- (/) |
|
| 4 | 3 | csn | |- { (/) } |
| 5 | 4 0 | cxp | |- ( { (/) } X. A ) |
| 6 | c1o | |- 1o |
|
| 7 | 6 | csn | |- { 1o } |
| 8 | 7 1 | cxp | |- ( { 1o } X. B ) |
| 9 | 5 8 | cun | |- ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) |
| 10 | 2 9 | wceq | |- ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) |