Definition df-dju 7228

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 7227	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3492	. . . . 5 class ∅
5	4	csn 3667	. . . 4 class {∅}
6	5, 1	cxp 4721	. . 3 class ({∅} × 𝐴)
7		c1o 6570	. . . . 5 class 1o
8	7	csn 3667	. . . 4 class {1o}
9	8, 2	cxp 4721	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3196	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1395	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7229  nfdju  7232  djuex  7233  djuexb  7234  djulclr  7239  djurclr  7240  djulcl  7241  djurcl  7242  djulclb  7245  djuunr  7256  eldju2ndl  7262  eldju2ndr  7263  xp2dju  7420  djucomen  7421  djuassen  7422  xpdjuen  7423  djulclALT  16333  djurclALT  16334