Definition df-dju 7097

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 7096	. 2 class ( A ⊔ B )
4		c0 3446	. . . . 5 class (/)
5	4	csn 3618	. . . 4 class { (/) }
6	5, 1	cxp 4657	. . 3 class ( { (/) } X. A )
7		c1o 6462	. . . . 5 class 1o
8	7	csn 3618	. . . 4 class { 1o }
9	8, 2	cxp 4657	. . 3 class ( { 1o } X. B )
10	6, 9	cun 3151	. 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  7098  nfdju  7101  djuex  7102  djuexb  7103  djulclr  7108  djurclr  7109  djulcl  7110  djurcl  7111  djulclb  7114  djuunr  7125  eldju2ndl  7131  eldju2ndr  7132  xp2dju  7275  djucomen  7276  djuassen  7277  xpdjuen  7278  djulclALT  15293  djurclALT  15294