![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-dju | GIF version |
Description: Disjoint union of two classes. This is a way of creating a class which contains elements corresponding to each element of 𝐴 or 𝐵, tagging each one with whether it came from 𝐴 or 𝐵. (Contributed by Jim Kingdon, 20-Jun-2022.) |
Ref | Expression |
---|---|
df-dju | ⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cdju 6872 | . 2 class (𝐴 ⊔ 𝐵) |
4 | c0 3327 | . . . . 5 class ∅ | |
5 | 4 | csn 3491 | . . . 4 class {∅} |
6 | 5, 1 | cxp 4495 | . . 3 class ({∅} × 𝐴) |
7 | c1o 6258 | . . . . 5 class 1o | |
8 | 7 | csn 3491 | . . . 4 class {1o} |
9 | 8, 2 | cxp 4495 | . . 3 class ({1o} × 𝐵) |
10 | 6, 9 | cun 3033 | . 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
11 | 3, 10 | wceq 1312 | 1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: djueq12 6874 nfdju 6877 djuex 6878 djuexb 6879 djulclr 6884 djurclr 6885 djulcl 6886 djurcl 6887 djulclb 6890 djuunr 6901 eldju2ndl 6907 eldju2ndr 6908 xp2dju 7016 djucomen 7017 djuassen 7018 xpdjuen 7019 djulclALT 12691 djurclALT 12692 |
Copyright terms: Public domain | W3C validator |