Definition df-dju 9861

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 9858	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4299	. . . . 5 class ∅
5	4	csn 4592	. . . 4 class {∅}
6	5, 1	cxp 5639	. . 3 class ({∅} × 𝐴)
7		c1o 8430	. . . . 5 class 1o
8	7	csn 4592	. . . 4 class {1o}
9	8, 2	cxp 5639	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3915	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1540	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9864  nfdju  9867  djuex  9868  djuexb  9869  djulcl  9870  djurcl  9871  djur  9879  djuunxp  9881  eldju2ndl  9884  eldju2ndr  9885  djuun  9886  undjudom  10128  endjudisj  10129  djuen  10130  dju1dif  10133  dju1p1e2  10134  xp2dju  10137  djucomen  10138  djuassen  10139  xpdjuen  10140  mapdjuen  10141  djudom1  10143  djuxpdom  10146  djufi  10147  djuinf  10149  infdju1  10150  ficardadju  10160  pwdjudom  10175  isfin4p1  10275  alephadd  10537  canthp1lem2  10613