Definition df-dju 7036

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 7035	. 2 class ( A ⊔ B )
4		c0 3422	. . . . 5 class (/)
5	4	csn 3592	. . . 4 class { (/) }
6	5, 1	cxp 4624	. . 3 class ( { (/) } X. A )
7		c1o 6409	. . . . 5 class 1o
8	7	csn 3592	. . . 4 class { 1o }
9	8, 2	cxp 4624	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3127	. 2 class ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
11	3, 10	wceq 1353	1 wff ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )

This definition is referenced by:  djueq12  7037  nfdju  7040  djuex  7041  djuexb  7042  djulclr  7047  djurclr  7048  djulcl  7049  djurcl  7050  djulclb  7053  djuunr  7064  eldju2ndl  7070  eldju2ndr  7071  xp2dju  7213  djucomen  7214  djuassen  7215  xpdjuen  7216  djulclALT  14523  djurclALT  14524