Definition df-dju 9938

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 9935	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4338	. . . . 5 class ∅
5	4	csn 4630	. . . 4 class {∅}
6	5, 1	cxp 5686	. . 3 class ({∅} × 𝐴)
7		c1o 8497	. . . . 5 class 1o
8	7	csn 4630	. . . 4 class {1o}
9	8, 2	cxp 5686	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3960	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1536	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9941  nfdju  9944  djuex  9945  djuexb  9946  djulcl  9947  djurcl  9948  djur  9956  djuunxp  9958  eldju2ndl  9961  eldju2ndr  9962  djuun  9963  undjudom  10205  endjudisj  10206  djuen  10207  dju1dif  10210  dju1p1e2  10211  xp2dju  10214  djucomen  10215  djuassen  10216  xpdjuen  10217  mapdjuen  10218  djudom1  10220  djuxpdom  10223  djufi  10224  djuinf  10226  infdju1  10227  ficardadju  10237  pwdjudom  10252  isfin4p1  10352  alephadd  10614  canthp1lem2  10690