Definition df-dju 9801

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 9798	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4282	. . . . 5 class ∅
5	4	csn 4575	. . . 4 class {∅}
6	5, 1	cxp 5617	. . 3 class ({∅} × 𝐴)
7		c1o 8384	. . . . 5 class 1o
8	7	csn 4575	. . . 4 class {1o}
9	8, 2	cxp 5617	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3896	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1541	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9804  nfdju  9807  djuex  9808  djuexb  9809  djulcl  9810  djurcl  9811  djur  9819  djuunxp  9821  eldju2ndl  9824  eldju2ndr  9825  djuun  9826  undjudom  10066  endjudisj  10067  djuen  10068  dju1dif  10071  dju1p1e2  10072  xp2dju  10075  djucomen  10076  djuassen  10077  xpdjuen  10078  mapdjuen  10079  djudom1  10081  djuxpdom  10084  djufi  10085  djuinf  10087  infdju1  10088  ficardadju  10098  pwdjudom  10113  isfin4p1  10213  alephadd  10475  canthp1lem2  10551