Definition df-dju 9941

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 9938	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4333	. . . . 5 class ∅
5	4	csn 4626	. . . 4 class {∅}
6	5, 1	cxp 5683	. . 3 class ({∅} × 𝐴)
7		c1o 8499	. . . . 5 class 1o
8	7	csn 4626	. . . 4 class {1o}
9	8, 2	cxp 5683	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3949	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1540	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9944  nfdju  9947  djuex  9948  djuexb  9949  djulcl  9950  djurcl  9951  djur  9959  djuunxp  9961  eldju2ndl  9964  eldju2ndr  9965  djuun  9966  undjudom  10208  endjudisj  10209  djuen  10210  dju1dif  10213  dju1p1e2  10214  xp2dju  10217  djucomen  10218  djuassen  10219  xpdjuen  10220  mapdjuen  10221  djudom1  10223  djuxpdom  10226  djufi  10227  djuinf  10229  infdju1  10230  ficardadju  10240  pwdjudom  10255  isfin4p1  10355  alephadd  10617  canthp1lem2  10693