Definition df-dju 9122

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 9119	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4172	. . . . 5 class ∅
5	4	csn 4435	. . . 4 class {∅}
6	5, 1	cxp 5401	. . 3 class ({∅} × 𝐴)
7		c1o 7896	. . . . 5 class 1o
8	7	csn 4435	. . . 4 class {1o}
9	8, 2	cxp 5401	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3820	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1508	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9125  nfdju  9128  djuex  9129  djuexb  9130  djulcl  9131  djurcl  9132  djur  9140  djuunxp  9142  eldju2ndl  9145  eldju2ndr  9146  djuun  9147  cdadju  9388  undjudom  9389  endjudisj  9390  djuen  9391  dju1dif  9394  dju1p1e2  9395  xp2dju  9398  djucomen  9399  djuassen  9400  xpdjuen  9401  mapdjuen  9402  djudom1  9404  djuxpdom  9407  djufi  9408  djuinf  9410  infdju1  9411  pwdjudom  9434  isfin4p1  9533  alephadd  9795  canthp1lem2  9871