Definition df-dju 7384

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 7383	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3520	. . . . 5 class ∅
5	4	csn 3709	. . . 4 class {∅}
6	5, 1	cxp 4774	. . 3 class ({∅} × 𝐴)
7		c1o 6684	. . . . 5 class 1o
8	7	csn 3709	. . . 4 class {1o}
9	8, 2	cxp 4774	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3218	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1402	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is used by:  djueq12  7385  nfdju  7388  djuex  7389  djuexb  7390  djulclr  7395  djurclr  7396  djulcl  7397  djurcl  7398  djulclb  7401  djuunr  7412  eldju2ndl  7418  eldju2ndr  7419  xp2dju  7577  djucomen  7578  djuassen  7579  xpdjuen  7580  djulclALT  17034  djurclALT  17035  idjudju  17252