Definition df-dju 9909

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 9906	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4279	. . . . 5 class ∅
5	4	csn 4584	. . . 4 class {∅}
6	5, 1	cxp 5653	. . 3 class ({∅} × 𝐴)
7		c1o 8451	. . . . 5 class 1o
8	7	csn 4584	. . . 4 class {1o}
9	8, 2	cxp 5653	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3897	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1570	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is used by:  djueq12  9912  nfdju  9915  djuex  9916  djuexb  9917  djulcl  9918  djurcl  9919  djur  9927  djuunxp  9929  eldju2ndl  9932  eldju2ndr  9933  djuun  9934  undjudom  10173  endjudisj  10174  djuen  10175  dju1dif  10178  dju1p1e2  10179  xp2dju  10182  djucomen  10183  djuassen  10184  xpdjuen  10185  mapdjuen  10186  djudom1  10188  djuxpdom  10191  djufi  10192  djuinf  10194  infdju1  10195  ficardadju  10205  pwdjudom  10220  isfin4p1  10320  alephadd  10589  canthp1lem2  10665