Definition df-dju 7040

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 7039	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3424	. . . . 5 class ∅
5	4	csn 3594	. . . 4 class {∅}
6	5, 1	cxp 4626	. . 3 class ({∅} × 𝐴)
7		c1o 6413	. . . . 5 class 1o
8	7	csn 3594	. . . 4 class {1o}
9	8, 2	cxp 4626	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3129	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1353	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7041  nfdju  7044  djuex  7045  djuexb  7046  djulclr  7051  djurclr  7052  djulcl  7053  djurcl  7054  djulclb  7057  djuunr  7068  eldju2ndl  7074  eldju2ndr  7075  xp2dju  7217  djucomen  7218  djuassen  7219  xpdjuen  7220  djulclALT  14714  djurclALT  14715