Definition df-dju 7368

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.)

Assertion

Ref	Expression
df-dju	⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

Detailed syntax breakdown of Definition df-dju

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cdju 7367	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3520	. . . . 5 class ∅
5	4	csn 3705	. . . 4 class {∅}
6	5, 1	cxp 4767	. . 3 class ({∅} × 𝐴)
7		c1o 6670	. . . . 5 class 1o
8	7	csn 3705	. . . 4 class {1o}
9	8, 2	cxp 4767	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3218	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1402	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7369  nfdju  7372  djuex  7373  djuexb  7374  djulclr  7379  djurclr  7380  djulcl  7381  djurcl  7382  djulclb  7385  djuunr  7396  eldju2ndl  7402  eldju2ndr  7403  xp2dju  7561  djucomen  7562  djuassen  7563  xpdjuen  7564  djulclALT  16743  djurclALT  16744