Definition df-dju 7236

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 7235	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3494	. . . . 5 class ∅
5	4	csn 3669	. . . 4 class {∅}
6	5, 1	cxp 4723	. . 3 class ({∅} × 𝐴)
7		c1o 6574	. . . . 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  7237  nfdju  7240  djuex  7241  djuexb  7242  djulclr  7247  djurclr  7248  djulcl  7249  djurcl  7250  djulclb  7253  djuunr  7264  eldju2ndl  7270  eldju2ndr  7271  xp2dju  7429  djucomen  7430  djuassen  7431  xpdjuen  7432  djulclALT  16397  djurclALT  16398