Definition df-dju 7104

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 7103	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3450	. . . . 5 class ∅
5	4	csn 3622	. . . 4 class {∅}
6	5, 1	cxp 4661	. . 3 class ({∅} × 𝐴)
7		c1o 6467	. . . . 5 class 1o
8	7	csn 3622	. . . 4 class {1o}
9	8, 2	cxp 4661	. . 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  7105  nfdju  7108  djuex  7109  djuexb  7110  djulclr  7115  djurclr  7116  djulcl  7117  djurcl  7118  djulclb  7121  djuunr  7132  eldju2ndl  7138  eldju2ndr  7139  xp2dju  7282  djucomen  7283  djuassen  7284  xpdjuen  7285  djulclALT  15447  djurclALT  15448