Definition df-dju 6976

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 6975	. 2 class ( A ⊔ B )
4		c0 3394	. . . . 5 class (/)
5	4	csn 3560	. . . 4 class { (/) }
6	5, 1	cxp 4583	. . 3 class ( { (/) } X. A )
7		c1o 6353	. . . . 5 class 1o
8	7	csn 3560	. . . 4 class { 1o }
9	8, 2	cxp 4583	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3100	. 2 class ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
11	3, 10	wceq 1335	1 wff ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )

This definition is referenced by:  djueq12  6977  nfdju  6980  djuex  6981  djuexb  6982  djulclr  6987  djurclr  6988  djulcl  6989  djurcl  6990  djulclb  6993  djuunr  7004  eldju2ndl  7010  eldju2ndr  7011  xp2dju  7144  djucomen  7145  djuassen  7146  xpdjuen  7147  djulclALT  13346  djurclALT  13347