Definition df-dju 7205

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 7204	. 2 class ( A ⊔ B )
4		c0 3491	. . . . 5 class (/)
5	4	csn 3666	. . . 4 class { (/) }
6	5, 1	cxp 4717	. . 3 class ( { (/) } X. A )
7		c1o 6555	. . . . 5 class 1o
8	7	csn 3666	. . . 4 class { 1o }
9	8, 2	cxp 4717	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3195	. 2 class ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
11	3, 10	wceq 1395	1 wff ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )

This definition is referenced by:  djueq12  7206  nfdju  7209  djuex  7210  djuexb  7211  djulclr  7216  djurclr  7217  djulcl  7218  djurcl  7219  djulclb  7222  djuunr  7233  eldju2ndl  7239  eldju2ndr  7240  xp2dju  7397  djucomen  7398  djuassen  7399  xpdjuen  7400  djulclALT  16165  djurclALT  16166