Definition df-dju 9995

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

This definition is used by:  djueq12  9998  nfdju  10001  djuex  10002  djuexb  10003  djulcl  10004  djurcl  10005  djur  10013  djuunxp  10015  eldju2ndl  10018  eldju2ndr  10019  djuun  10020  undjudom  10259  endjudisj  10260  djuen  10261  dju1dif  10264  dju1p1e2  10265  xp2dju  10268  djucomen  10269  djuassen  10270  xpdjuen  10271  mapdjuen  10272  djudom1  10274  djuxpdom  10277  djufi  10278  djuinf  10280  infdju1  10281  ficardadju  10291  pwdjudom  10306  isfin4p1  10406  alephadd  10675  canthp1lem2  10751