Definition df-dju 9883

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 9880	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4286	. . . . 5 class ∅
5	4	csn 4589	. . . 4 class {∅}
6	5, 1	cxp 5659	. . 3 class ({∅} × 𝐴)
7		c1o 8442	. . . . 5 class 1o
8	7	csn 4589	. . . 4 class {1o}
9	8, 2	cxp 5659	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3903	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1570	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9886  nfdju  9889  djuex  9890  djuexb  9891  djulcl  9892  djurcl  9893  djur  9901  djuunxp  9903  eldju2ndl  9906  eldju2ndr  9907  djuun  9908  undjudom  10147  endjudisj  10148  djuen  10149  dju1dif  10152  dju1p1e2  10153  xp2dju  10156  djucomen  10157  djuassen  10158  xpdjuen  10159  mapdjuen  10160  djudom1  10162  djuxpdom  10165  djufi  10166  djuinf  10168  infdju1  10169  ficardadju  10179  pwdjudom  10194  isfin4p1  10294  alephadd  10557  canthp1lem2  10633