Definition df-dju 9913

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 9910	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4308	. . . . 5 class ∅
5	4	csn 4601	. . . 4 class {∅}
6	5, 1	cxp 5652	. . 3 class ({∅} × 𝐴)
7		c1o 8471	. . . . 5 class 1o
8	7	csn 4601	. . . 4 class {1o}
9	8, 2	cxp 5652	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3924	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1540	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9916  nfdju  9919  djuex  9920  djuexb  9921  djulcl  9922  djurcl  9923  djur  9931  djuunxp  9933  eldju2ndl  9936  eldju2ndr  9937  djuun  9938  undjudom  10180  endjudisj  10181  djuen  10182  dju1dif  10185  dju1p1e2  10186  xp2dju  10189  djucomen  10190  djuassen  10191  xpdjuen  10192  mapdjuen  10193  djudom1  10195  djuxpdom  10198  djufi  10199  djuinf  10201  infdju1  10202  ficardadju  10212  pwdjudom  10227  isfin4p1  10327  alephadd  10589  canthp1lem2  10665