Definition df-dju 7280

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 7279	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3496	. . . . 5 class ∅
5	4	csn 3673	. . . 4 class {∅}
6	5, 1	cxp 4729	. . 3 class ({∅} × 𝐴)
7		c1o 6618	. . . . 5 class 1o
8	7	csn 3673	. . . 4 class {1o}
9	8, 2	cxp 4729	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3199	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1398	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7281  nfdju  7284  djuex  7285  djuexb  7286  djulclr  7291  djurclr  7292  djulcl  7293  djurcl  7294  djulclb  7297  djuunr  7308  eldju2ndl  7314  eldju2ndr  7315  xp2dju  7473  djucomen  7474  djuassen  7475  xpdjuen  7476  djulclALT  16502  djurclALT  16503