Definition df-dju 7142

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 7141	. 2 class ( A ⊔ B )
4		c0 3460	. . . . 5 class (/)
5	4	csn 3633	. . . 4 class { (/) }
6	5, 1	cxp 4674	. . 3 class ( { (/) } X. A )
7		c1o 6497	. . . . 5 class 1o
8	7	csn 3633	. . . 4 class { 1o }
9	8, 2	cxp 4674	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3164	. 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  7143  nfdju  7146  djuex  7147  djuexb  7148  djulclr  7153  djurclr  7154  djulcl  7155  djurcl  7156  djulclb  7159  djuunr  7170  eldju2ndl  7176  eldju2ndr  7177  xp2dju  7329  djucomen  7330  djuassen  7331  xpdjuen  7332  djulclALT  15774  djurclALT  15775