Definition df-dju 7067

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 7066	. 2 class ( A ⊔ B )
4		c0 3437	. . . . 5 class (/)
5	4	csn 3607	. . . 4 class { (/) }
6	5, 1	cxp 4642	. . 3 class ( { (/) } X. A )
7		c1o 6434	. . . . 5 class 1o
8	7	csn 3607	. . . 4 class { 1o }
9	8, 2	cxp 4642	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3142	. 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  7068  nfdju  7071  djuex  7072  djuexb  7073  djulclr  7078  djurclr  7079  djulcl  7080  djurcl  7081  djulclb  7084  djuunr  7095  eldju2ndl  7101  eldju2ndr  7102  xp2dju  7244  djucomen  7245  djuassen  7246  xpdjuen  7247  djulclALT  15014  djurclALT  15015