Definition df-dju 9859

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 9856	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4285	. . . . 5 class ∅
5	4	csn 4582	. . . 4 class {∅}
6	5, 1	cxp 5645	. . 3 class ({∅} × 𝐴)
7		c1o 8430	. . . . 5 class 1o
8	7	csn 4582	. . . 4 class {1o}
9	8, 2	cxp 5645	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3902	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1560	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9862  nfdju  9865  djuex  9866  djuexb  9867  djulcl  9868  djurcl  9869  djur  9877  djuunxp  9879  eldju2ndl  9882  eldju2ndr  9883  djuun  9884  undjudom  10124  endjudisj  10125  djuen  10126  dju1dif  10129  dju1p1e2  10130  xp2dju  10133  djucomen  10134  djuassen  10135  xpdjuen  10136  mapdjuen  10137  djudom1  10139  djuxpdom  10142  djufi  10143  djuinf  10145  infdju1  10146  ficardadju  10156  pwdjudom  10171  isfin4p1  10272  alephadd  10535  canthp1lem2  10611