Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-dju | Unicode 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 | ⊔ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | cdju 6922 | . 2 ⊔ |
4 | c0 3363 | . . . . 5 | |
5 | 4 | csn 3527 | . . . 4 |
6 | 5, 1 | cxp 4537 | . . 3 |
7 | c1o 6306 | . . . . 5 | |
8 | 7 | csn 3527 | . . . 4 |
9 | 8, 2 | cxp 4537 | . . 3 |
10 | 6, 9 | cun 3069 | . 2 |
11 | 3, 10 | wceq 1331 | 1 ⊔ |
Colors of variables: wff set class |
This definition is referenced by: djueq12 6924 nfdju 6927 djuex 6928 djuexb 6929 djulclr 6934 djurclr 6935 djulcl 6936 djurcl 6937 djulclb 6940 djuunr 6951 eldju2ndl 6957 eldju2ndr 6958 xp2dju 7071 djucomen 7072 djuassen 7073 xpdjuen 7074 djulclALT 13008 djurclALT 13009 |
Copyright terms: Public domain | W3C validator |