Definition df-dju 7237

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 7236	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3494	. . . . 5 class ∅
5	4	csn 3669	. . . 4 class {∅}
6	5, 1	cxp 4723	. . 3 class ({∅} × 𝐴)
7		c1o 6575	. . . . 5 class 1o
8	7	csn 3669	. . . 4 class {1o}
9	8, 2	cxp 4723	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3198	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1397	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7238  nfdju  7241  djuex  7242  djuexb  7243  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  djulclb  7254  djuunr  7265  eldju2ndl  7271  eldju2ndr  7272  xp2dju  7430  djucomen  7431  djuassen  7432  xpdjuen  7433  djulclALT  16448  djurclALT  16449