Definition df-dju 6923

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 6922	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3363	. . . . 5 class ∅
5	4	csn 3527	. . . 4 class {∅}
6	5, 1	cxp 4537	. . 3 class ({∅} × 𝐴)
7		c1o 6306	. . . . 5 class 1o
8	7	csn 3527	. . . 4 class {1o}
9	8, 2	cxp 4537	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3069	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1331	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  6924  nfdju  6927  djuex  6928  djuexb  6929  djulclr  6934  djurclr  6935  djulcl  6936  djurcl  6937  djulclb  6940  djuunr  6951  eldju2ndl  6957  eldju2ndr  6958  xp2dju  7071  djucomen  7072  djuassen  7073  xpdjuen  7074  djulclALT  13008  djurclALT  13009