![]() |
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 | ⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cdju 6730 | . 2 class (𝐴 ⊔ 𝐵) |
4 | c0 3286 | . . . . 5 class ∅ | |
5 | 4 | csn 3446 | . . . 4 class {∅} |
6 | 5, 1 | cxp 4436 | . . 3 class ({∅} × 𝐴) |
7 | c1o 6174 | . . . . 5 class 1𝑜 | |
8 | 7 | csn 3446 | . . . 4 class {1𝑜} |
9 | 8, 2 | cxp 4436 | . . 3 class ({1𝑜} × 𝐵) |
10 | 6, 9 | cun 2997 | . 2 class (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵)) |
11 | 3, 10 | wceq 1289 | 1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: djueq12 6732 nfdju 6735 djuex 6736 djulclr 6741 djurclr 6742 djulcl 6743 djurcl 6744 djulclb 6747 djur 6757 djuunr 6758 eldju2ndl 6763 eldju2ndr 6764 djulclALT 11701 djurclALT 11702 |
Copyright terms: Public domain | W3C validator |