Definition df-dju 9816

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 9813	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4286	. . . . 5 class ∅
5	4	csn 4579	. . . 4 class {∅}
6	5, 1	cxp 5621	. . 3 class ({∅} × 𝐴)
7		c1o 8388	. . . . 5 class 1o
8	7	csn 4579	. . . 4 class {1o}
9	8, 2	cxp 5621	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3903	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1540	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9819  nfdju  9822  djuex  9823  djuexb  9824  djulcl  9825  djurcl  9826  djur  9834  djuunxp  9836  eldju2ndl  9839  eldju2ndr  9840  djuun  9841  undjudom  10081  endjudisj  10082  djuen  10083  dju1dif  10086  dju1p1e2  10087  xp2dju  10090  djucomen  10091  djuassen  10092  xpdjuen  10093  mapdjuen  10094  djudom1  10096  djuxpdom  10099  djufi  10100  djuinf  10102  infdju1  10103  ficardadju  10113  pwdjudom  10128  isfin4p1  10228  alephadd  10490  canthp1lem2  10566