Definition df-dju 7140

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 7139	. 2 class ( A ⊔ B )
4		c0 3460	. . . . 5 class (/)
5	4	csn 3633	. . . 4 class { (/) }
6	5, 1	cxp 4673	. . 3 class ( { (/) } X. A )
7		c1o 6495	. . . . 5 class 1o
8	7	csn 3633	. . . 4 class { 1o }
9	8, 2	cxp 4673	. . 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  7141  nfdju  7144  djuex  7145  djuexb  7146  djulclr  7151  djurclr  7152  djulcl  7153  djurcl  7154  djulclb  7157  djuunr  7168  eldju2ndl  7174  eldju2ndr  7175  xp2dju  7327  djucomen  7328  djuassen  7329  xpdjuen  7330  djulclALT  15737  djurclALT  15738