Definition df-dju 9854

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 9851	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4296	. . . . 5 class ∅
5	4	csn 4589	. . . 4 class {∅}
6	5, 1	cxp 5636	. . 3 class ({∅} × 𝐴)
7		c1o 8427	. . . . 5 class 1o
8	7	csn 4589	. . . 4 class {1o}
9	8, 2	cxp 5636	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3912	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1540	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9857  nfdju  9860  djuex  9861  djuexb  9862  djulcl  9863  djurcl  9864  djur  9872  djuunxp  9874  eldju2ndl  9877  eldju2ndr  9878  djuun  9879  undjudom  10121  endjudisj  10122  djuen  10123  dju1dif  10126  dju1p1e2  10127  xp2dju  10130  djucomen  10131  djuassen  10132  xpdjuen  10133  mapdjuen  10134  djudom1  10136  djuxpdom  10139  djufi  10140  djuinf  10142  infdju1  10143  ficardadju  10153  pwdjudom  10168  isfin4p1  10268  alephadd  10530  canthp1lem2  10606