Definition df-dju 7378

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 7377	. 2 class ( A ⊔ B )
4		c0 3520	. . . . 5 class (/)
5	4	csn 3709	. . . 4 class { (/) }
6	5, 1	cxp 4772	. . 3 class ( { (/) } X. A )
7		c1o 6680	. . . . 5 class 1o
8	7	csn 3709	. . . 4 class { 1o }
9	8, 2	cxp 4772	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3218	. 2 class ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
11	3, 10	wceq 1402	1 wff ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )

This definition is used by:  djueq12  7379  nfdju  7382  djuex  7383  djuexb  7384  djulclr  7389  djurclr  7390  djulcl  7391  djurcl  7392  djulclb  7395  djuunr  7406  eldju2ndl  7412  eldju2ndr  7413  xp2dju  7571  djucomen  7572  djuassen  7573  xpdjuen  7574  djulclALT  16829  djurclALT  16830