Definition df-dju 7099

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 7098	. 2 class ( A ⊔ B )
4		c0 3447	. . . . 5 class (/)
5	4	csn 3619	. . . 4 class { (/) }
6	5, 1	cxp 4658	. . 3 class ( { (/) } X. A )
7		c1o 6464	. . . . 5 class 1o
8	7	csn 3619	. . . 4 class { 1o }
9	8, 2	cxp 4658	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3152	. 2 class ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
11	3, 10	wceq 1364	1 wff ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )

This definition is referenced by:  djueq12  7100  nfdju  7103  djuex  7104  djuexb  7105  djulclr  7110  djurclr  7111  djulcl  7112  djurcl  7113  djulclb  7116  djuunr  7127  eldju2ndl  7133  eldju2ndr  7134  xp2dju  7277  djucomen  7278  djuassen  7279  xpdjuen  7280  djulclALT  15363  djurclALT  15364