Definition df-dju 7216

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 7215	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3491	. . . . 5 class ∅
5	4	csn 3666	. . . 4 class {∅}
6	5, 1	cxp 4717	. . 3 class ({∅} × 𝐴)
7		c1o 6561	. . . . 5 class 1o
8	7	csn 3666	. . . 4 class {1o}
9	8, 2	cxp 4717	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3195	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1395	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7217  nfdju  7220  djuex  7221  djuexb  7222  djulclr  7227  djurclr  7228  djulcl  7229  djurcl  7230  djulclb  7233  djuunr  7244  eldju2ndl  7250  eldju2ndr  7251  xp2dju  7408  djucomen  7409  djuassen  7410  xpdjuen  7411  djulclALT  16220  djurclALT  16221