Definition df-dju 7037

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 7036	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3423	. . . . 5 class ∅
5	4	csn 3593	. . . 4 class {∅}
6	5, 1	cxp 4625	. . 3 class ({∅} × 𝐴)
7		c1o 6410	. . . . 5 class 1o
8	7	csn 3593	. . . 4 class {1o}
9	8, 2	cxp 4625	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3128	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1353	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7038  nfdju  7041  djuex  7042  djuexb  7043  djulclr  7048  djurclr  7049  djulcl  7050  djurcl  7051  djulclb  7054  djuunr  7065  eldju2ndl  7071  eldju2ndr  7072  xp2dju  7214  djucomen  7215  djuassen  7216  xpdjuen  7217  djulclALT  14556  djurclALT  14557