Definition df-dju 7329

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 7328	. 2 class ( A ⊔ B )
4		c0 3508	. . . . 5 class (/)
5	4	csn 3689	. . . 4 class { (/) }
6	5, 1	cxp 4747	. . 3 class ( { (/) } X. A )
7		c1o 6640	. . . . 5 class 1o
8	7	csn 3689	. . . 4 class { 1o }
9	8, 2	cxp 4747	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3209	. 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  7330  nfdju  7333  djuex  7334  djuexb  7335  djulclr  7340  djurclr  7341  djulcl  7342  djurcl  7343  djulclb  7346  djuunr  7357  eldju2ndl  7363  eldju2ndr  7364  xp2dju  7522  djucomen  7523  djuassen  7524  xpdjuen  7525  djulclALT  16573  djurclALT  16574