Definition df-dju 7297

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 7296	. 2 class ( A ⊔ B )
4		c0 3496	. . . . 5 class (/)
5	4	csn 3673	. . . 4 class { (/) }
6	5, 1	cxp 4729	. . 3 class ( { (/) } X. A )
7		c1o 6618	. . . . 5 class 1o
8	7	csn 3673	. . . 4 class { 1o }
9	8, 2	cxp 4729	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3199	. 2 class ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
11	3, 10	wceq 1398	1 wff ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )

This definition is referenced by:  djueq12  7298  nfdju  7301  djuex  7302  djuexb  7303  djulclr  7308  djurclr  7309  djulcl  7310  djurcl  7311  djulclb  7314  djuunr  7325  eldju2ndl  7331  eldju2ndr  7332  xp2dju  7490  djucomen  7491  djuassen  7492  xpdjuen  7493  djulclALT  16519  djurclALT  16520