Definition df-dju 9330

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 9327	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4291	. . . . 5 class ∅
5	4	csn 4567	. . . 4 class {∅}
6	5, 1	cxp 5553	. . 3 class ({∅} × 𝐴)
7		c1o 8095	. . . . 5 class 1o
8	7	csn 4567	. . . 4 class {1o}
9	8, 2	cxp 5553	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3934	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1537	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9333  nfdju  9336  djuex  9337  djuexb  9338  djulcl  9339  djurcl  9340  djur  9348  djuunxp  9350  eldju2ndl  9353  eldju2ndr  9354  djuun  9355  undjudom  9593  endjudisj  9594  djuen  9595  dju1dif  9598  dju1p1e2  9599  xp2dju  9602  djucomen  9603  djuassen  9604  xpdjuen  9605  mapdjuen  9606  djudom1  9608  djuxpdom  9611  djufi  9612  djuinf  9614  infdju1  9615  pwdjudom  9638  isfin4p1  9737  alephadd  9999  canthp1lem2  10075