Definition df-dju 7331

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 7330	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3510	. . . . 5 class ∅
5	4	csn 3691	. . . 4 class {∅}
6	5, 1	cxp 4749	. . 3 class ({∅} × 𝐴)
7		c1o 6642	. . . . 5 class 1o
8	7	csn 3691	. . . 4 class {1o}
9	8, 2	cxp 4749	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3211	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1398	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7332  nfdju  7335  djuex  7336  djuexb  7337  djulclr  7342  djurclr  7343  djulcl  7344  djurcl  7345  djulclb  7348  djuunr  7359  eldju2ndl  7365  eldju2ndr  7366  xp2dju  7524  djucomen  7525  djuassen  7526  xpdjuen  7527  djulclALT  16590  djurclALT  16591