Definition df-dju 7113

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 7112	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3451	. . . . 5 class ∅
5	4	csn 3623	. . . 4 class {∅}
6	5, 1	cxp 4662	. . 3 class ({∅} × 𝐴)
7		c1o 6476	. . . . 5 class 1o
8	7	csn 3623	. . . 4 class {1o}
9	8, 2	cxp 4662	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3155	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1364	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7114  nfdju  7117  djuex  7118  djuexb  7119  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  djulclb  7130  djuunr  7141  eldju2ndl  7147  eldju2ndr  7148  xp2dju  7298  djucomen  7299  djuassen  7300  xpdjuen  7301  djulclALT  15531  djurclALT  15532