Definition df-dju 9825

Description: Disjoint union of two classes. This is a way of creating a set which contains elements corresponding to each element of 𝐴 or 𝐵, tagging each one with whether it came from 𝐴 or 𝐵. (Contributed by Jim Kingdon, 20-Jun-2022.)

Assertion

Ref	Expression
df-dju	⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

Detailed syntax breakdown of Definition df-dju

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cdju 9822	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4287	. . . . 5 class ∅
5	4	csn 4582	. . . 4 class {∅}
6	5, 1	cxp 5630	. . 3 class ({∅} × 𝐴)
7		c1o 8400	. . . . 5 class 1o
8	7	csn 4582	. . . 4 class {1o}
9	8, 2	cxp 5630	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3901	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1542	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9828  nfdju  9831  djuex  9832  djuexb  9833  djulcl  9834  djurcl  9835  djur  9843  djuunxp  9845  eldju2ndl  9848  eldju2ndr  9849  djuun  9850  undjudom  10090  endjudisj  10091  djuen  10092  dju1dif  10095  dju1p1e2  10096  xp2dju  10099  djucomen  10100  djuassen  10101  xpdjuen  10102  mapdjuen  10103  djudom1  10105  djuxpdom  10108  djufi  10109  djuinf  10111  infdju1  10112  ficardadju  10122  pwdjudom  10137  isfin4p1  10237  alephadd  10500  canthp1lem2  10576