Definition df-dju 7155

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 7154	. 2 class (𝐴 ⊔ 𝐵)
4		c0 3464	. . . . 5 class ∅
5	4	csn 3638	. . . 4 class {∅}
6	5, 1	cxp 4681	. . 3 class ({∅} × 𝐴)
7		c1o 6508	. . . . 5 class 1o
8	7	csn 3638	. . . 4 class {1o}
9	8, 2	cxp 4681	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3168	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1373	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  7156  nfdju  7159  djuex  7160  djuexb  7161  djulclr  7166  djurclr  7167  djulcl  7168  djurcl  7169  djulclb  7172  djuunr  7183  eldju2ndl  7189  eldju2ndr  7190  xp2dju  7343  djucomen  7344  djuassen  7345  xpdjuen  7346  djulclALT  15876  djurclALT  15877