Definition df-dju 7379

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 7378	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3520	. . . . 5 class ∅
5	4	csn 3709	. . . 4 class {∅}
6	5, 1	cxp 4772	. . 3 class ({∅} × 𝐴)
7		c1o 6680	. . . . 5 class 1o
8	7	csn 3709	. . . 4 class {1o}
9	8, 2	cxp 4772	. . 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  7380  nfdju  7383  djuex  7384  djuexb  7385  djulclr  7390  djurclr  7391  djulcl  7392  djurcl  7393  djulclb  7396  djuunr  7407  eldju2ndl  7413  eldju2ndr  7414  xp2dju  7572  djucomen  7573  djuassen  7574  xpdjuen  7575  djulclALT  16995  djurclALT  16996