Definition df-dju 9830

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 9827	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4292	. . . . 5 class ∅
5	4	csn 4585	. . . 4 class {∅}
6	5, 1	cxp 5629	. . 3 class ({∅} × 𝐴)
7		c1o 8404	. . . . 5 class 1o
8	7	csn 4585	. . . 4 class {1o}
9	8, 2	cxp 5629	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3909	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1540	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9833  nfdju  9836  djuex  9837  djuexb  9838  djulcl  9839  djurcl  9840  djur  9848  djuunxp  9850  eldju2ndl  9853  eldju2ndr  9854  djuun  9855  undjudom  10097  endjudisj  10098  djuen  10099  dju1dif  10102  dju1p1e2  10103  xp2dju  10106  djucomen  10107  djuassen  10108  xpdjuen  10109  mapdjuen  10110  djudom1  10112  djuxpdom  10115  djufi  10116  djuinf  10118  infdju1  10119  ficardadju  10129  pwdjudom  10144  isfin4p1  10244  alephadd  10506  canthp1lem2  10582