Definition df-dju 7027

Description: Disjoint union of two classes. This is a way of creating a class which contains elements corresponding to each element of A or B, tagging each one with whether it came from A or B. (Contributed by Jim Kingdon, 20-Jun-2022.)

Assertion

Ref	Expression
df-dju	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )

Detailed syntax breakdown of Definition df-dju

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cdju 7026	. 2 class ( A ⊔ B )
4		c0 3420	. . . . 5 class (/)
5	4	csn 3589	. . . 4 class { (/) }
6	5, 1	cxp 4618	. . 3 class ( { (/) } X. A )
7		c1o 6400	. . . . 5 class 1o
8	7	csn 3589	. . . 4 class { 1o }
9	8, 2	cxp 4618	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3125	. 2 class ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
11	3, 10	wceq 1353	1 wff ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )

This definition is referenced by:  djueq12  7028  nfdju  7031  djuex  7032  djuexb  7033  djulclr  7038  djurclr  7039  djulcl  7040  djurcl  7041  djulclb  7044  djuunr  7055  eldju2ndl  7061  eldju2ndr  7062  xp2dju  7204  djucomen  7205  djuassen  7206  xpdjuen  7207  djulclALT  14111  djurclALT  14112