Definition df-dju 9903

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

This definition is used by:  djueq12  9906  nfdju  9909  djuex  9910  djuexb  9911  djulcl  9912  djurcl  9913  djur  9921  djuunxp  9923  eldju2ndl  9926  eldju2ndr  9927  djuun  9928  undjudom  10167  endjudisj  10168  djuen  10169  dju1dif  10172  dju1p1e2  10173  xp2dju  10176  djucomen  10177  djuassen  10178  xpdjuen  10179  mapdjuen  10180  djudom1  10182  djuxpdom  10185  djufi  10186  djuinf  10188  infdju1  10189  ficardadju  10199  pwdjudom  10214  isfin4p1  10314  alephadd  10581  canthp1lem2  10657