Definition df-dju 7342

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 7341	. 2 class ( A ⊔ B )
4		c0 3512	. . . . 5 class (/)
5	4	csn 3694	. . . 4 class { (/) }
6	5, 1	cxp 4752	. . 3 class ( { (/) } X. A )
7		c1o 6653	. . . . 5 class 1o
8	7	csn 3694	. . . 4 class { 1o }
9	8, 2	cxp 4752	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3212	. 2 class ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
11	3, 10	wceq 1398	1 wff ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )

This definition is referenced by:  djueq12  7343  nfdju  7346  djuex  7347  djuexb  7348  djulclr  7353  djurclr  7354  djulcl  7355  djurcl  7356  djulclb  7359  djuunr  7370  eldju2ndl  7376  eldju2ndr  7377  xp2dju  7535  djucomen  7536  djuassen  7537  xpdjuen  7538  djulclALT  16699  djurclALT  16700