Definition df-dju 9896

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 9893	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4323	. . . . 5 class ∅
5	4	csn 4629	. . . 4 class {∅}
6	5, 1	cxp 5675	. . 3 class ({∅} × 𝐴)
7		c1o 8459	. . . . 5 class 1o
8	7	csn 4629	. . . 4 class {1o}
9	8, 2	cxp 5675	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3947	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1542	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9899  nfdju  9902  djuex  9903  djuexb  9904  djulcl  9905  djurcl  9906  djur  9914  djuunxp  9916  eldju2ndl  9919  eldju2ndr  9920  djuun  9921  undjudom  10162  endjudisj  10163  djuen  10164  dju1dif  10167  dju1p1e2  10168  xp2dju  10171  djucomen  10172  djuassen  10173  xpdjuen  10174  mapdjuen  10175  djudom1  10177  djuxpdom  10180  djufi  10181  djuinf  10183  infdju1  10184  ficardadju  10194  pwdjudom  10211  isfin4p1  10310  alephadd  10572  canthp1lem2  10648