Definition df-dju 6999

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 6998	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3408	. . . . 5 class ∅
5	4	csn 3575	. . . 4 class {∅}
6	5, 1	cxp 4601	. . 3 class ({∅} × 𝐴)
7		c1o 6373	. . . . 5 class 1o
8	7	csn 3575	. . . 4 class {1o}
9	8, 2	cxp 4601	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3113	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1343	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7000  nfdju  7003  djuex  7004  djuexb  7005  djulclr  7010  djurclr  7011  djulcl  7012  djurcl  7013  djulclb  7016  djuunr  7027  eldju2ndl  7033  eldju2ndr  7034  xp2dju  7167  djucomen  7168  djuassen  7169  xpdjuen  7170  djulclALT  13642  djurclALT  13643