Definition df-dju 6875

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 6874	. 2 class ( A ⊔ B )
4		c0 3329	. . . . 5 class (/)
5	4	csn 3493	. . . 4 class { (/) }
6	5, 1	cxp 4497	. . 3 class ( { (/) } X. A )
7		c1o 6260	. . . . 5 class 1o
8	7	csn 3493	. . . 4 class { 1o }
9	8, 2	cxp 4497	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3035	. 2 class ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
11	3, 10	wceq 1314	1 wff ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )

This definition is referenced by:  djueq12  6876  nfdju  6879  djuex  6880  djuexb  6881  djulclr  6886  djurclr  6887  djulcl  6888  djurcl  6889  djulclb  6892  djuunr  6903  eldju2ndl  6909  eldju2ndr  6910  xp2dju  7019  djucomen  7020  djuassen  7021  xpdjuen  7022  djulclALT  12700  djurclALT  12701