Definition df-dju 7166

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 7165	. 2 class ( A ⊔ B )
4		c0 3468	. . . . 5 class (/)
5	4	csn 3643	. . . 4 class { (/) }
6	5, 1	cxp 4691	. . 3 class ( { (/) } X. A )
7		c1o 6518	. . . . 5 class 1o
8	7	csn 3643	. . . 4 class { 1o }
9	8, 2	cxp 4691	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3172	. 2 class ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
11	3, 10	wceq 1373	1 wff ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )

This definition is referenced by:  djueq12  7167  nfdju  7170  djuex  7171  djuexb  7172  djulclr  7177  djurclr  7178  djulcl  7179  djurcl  7180  djulclb  7183  djuunr  7194  eldju2ndl  7200  eldju2ndr  7201  xp2dju  7358  djucomen  7359  djuassen  7360  xpdjuen  7361  djulclALT  15937  djurclALT  15938