Definition df-dju 6731

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	⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵))

Detailed syntax breakdown of Definition df-dju

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cdju 6730	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3286	. . . . 5 class ∅
5	4	csn 3446	. . . 4 class {∅}
6	5, 1	cxp 4436	. . 3 class ({∅} × 𝐴)
7		c1o 6174	. . . . 5 class 1𝑜
8	7	csn 3446	. . . 4 class {1𝑜}
9	8, 2	cxp 4436	. . 3 class ({1𝑜} × 𝐵)
10	6, 9	cun 2997	. 2 class (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵))
11	3, 10	wceq 1289	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵))

This definition is referenced by:  djueq12  6732  nfdju  6735  djuex  6736  djulclr  6741  djurclr  6742  djulcl  6743  djurcl  6744  djulclb  6747  djur  6757  djuunr  6758  eldju2ndl  6763  eldju2ndr  6764  djulclALT  11701  djurclALT  11702