Definition df-dju 9894

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

This definition is used by:  djueq12  9897  nfdju  9900  djuex  9901  djuexb  9902  djulcl  9903  djurcl  9904  djur  9912  djuunxp  9914  eldju2ndl  9917  eldju2ndr  9918  djuun  9919  undjudom  10158  endjudisj  10159  djuen  10160  dju1dif  10163  dju1p1e2  10164  xp2dju  10167  djucomen  10168  djuassen  10169  xpdjuen  10170  mapdjuen  10171  djudom1  10173  djuxpdom  10176  djufi  10177  djuinf  10179  infdju1  10180  ficardadju  10190  pwdjudom  10205  isfin4p1  10305  alephadd  10568  canthp1lem2  10644