Definition df-dju 7122

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 7121	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3459	. . . . 5 class ∅
5	4	csn 3632	. . . 4 class {∅}
6	5, 1	cxp 4671	. . 3 class ({∅} × 𝐴)
7		c1o 6485	. . . . 5 class 1o
8	7	csn 3632	. . . 4 class {1o}
9	8, 2	cxp 4671	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3163	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1372	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7123  nfdju  7126  djuex  7127  djuexb  7128  djulclr  7133  djurclr  7134  djulcl  7135  djurcl  7136  djulclb  7139  djuunr  7150  eldju2ndl  7156  eldju2ndr  7157  xp2dju  7309  djucomen  7310  djuassen  7311  xpdjuen  7312  djulclALT  15601  djurclALT  15602