Definition df-dju 9846

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 9843	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4287	. . . . 5 class ∅
5	4	csn 4591	. . . 4 class {∅}
6	5, 1	cxp 5636	. . 3 class ({∅} × 𝐴)
7		c1o 8410	. . . . 5 class 1o
8	7	csn 4591	. . . 4 class {1o}
9	8, 2	cxp 5636	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3911	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1541	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9849  nfdju  9852  djuex  9853  djuexb  9854  djulcl  9855  djurcl  9856  djur  9864  djuunxp  9866  eldju2ndl  9869  eldju2ndr  9870  djuun  9871  undjudom  10112  endjudisj  10113  djuen  10114  dju1dif  10117  dju1p1e2  10118  xp2dju  10121  djucomen  10122  djuassen  10123  xpdjuen  10124  mapdjuen  10125  djudom1  10127  djuxpdom  10130  djufi  10131  djuinf  10133  infdju1  10134  ficardadju  10144  pwdjudom  10161  isfin4p1  10260  alephadd  10522  canthp1lem2  10598