Definition df-dju 9887

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 9884	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4294	. . . . 5 class ∅
5	4	csn 4594	. . . 4 class {∅}
6	5, 1	cxp 5660	. . 3 class ({∅} × 𝐴)
7		c1o 8446	. . . . 5 class 1o
8	7	csn 4594	. . . 4 class {1o}
9	8, 2	cxp 5660	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3911	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1567	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9890  nfdju  9893  djuex  9894  djuexb  9895  djulcl  9896  djurcl  9897  djur  9905  djuunxp  9907  eldju2ndl  9910  eldju2ndr  9911  djuun  9912  undjudom  10151  endjudisj  10152  djuen  10153  dju1dif  10156  dju1p1e2  10157  xp2dju  10160  djucomen  10161  djuassen  10162  xpdjuen  10163  mapdjuen  10164  djudom1  10166  djuxpdom  10169  djufi  10170  djuinf  10172  infdju1  10173  ficardadju  10183  pwdjudom  10198  isfin4p1  10299  alephadd  10562  canthp1lem2  10638