Definition df-dju 6931

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 6930	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3368	. . . . 5 class ∅
5	4	csn 3532	. . . 4 class {∅}
6	5, 1	cxp 4545	. . 3 class ({∅} × 𝐴)
7		c1o 6314	. . . . 5 class 1o
8	7	csn 3532	. . . 4 class {1o}
9	8, 2	cxp 4545	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3074	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1332	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  6932  nfdju  6935  djuex  6936  djuexb  6937  djulclr  6942  djurclr  6943  djulcl  6944  djurcl  6945  djulclb  6948  djuunr  6959  eldju2ndl  6965  eldju2ndr  6966  xp2dju  7088  djucomen  7089  djuassen  7090  xpdjuen  7091  djulclALT  13179  djurclALT  13180