Definition df-dju 7201

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 7200	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3491	. . . . 5 class ∅
5	4	csn 3666	. . . 4 class {∅}
6	5, 1	cxp 4716	. . 3 class ({∅} × 𝐴)
7		c1o 6553	. . . . 5 class 1o
8	7	csn 3666	. . . 4 class {1o}
9	8, 2	cxp 4716	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3195	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1395	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7202  nfdju  7205  djuex  7206  djuexb  7207  djulclr  7212  djurclr  7213  djulcl  7214  djurcl  7215  djulclb  7218  djuunr  7229  eldju2ndl  7235  eldju2ndr  7236  xp2dju  7393  djucomen  7394  djuassen  7395  xpdjuen  7396  djulclALT  16123  djurclALT  16124