Definition df-dju 9970

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 9967	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4352	. . . . 5 class ∅
5	4	csn 4648	. . . 4 class {∅}
6	5, 1	cxp 5698	. . 3 class ({∅} × 𝐴)
7		c1o 8515	. . . . 5 class 1o
8	7	csn 4648	. . . 4 class {1o}
9	8, 2	cxp 5698	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3974	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1537	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9973  nfdju  9976  djuex  9977  djuexb  9978  djulcl  9979  djurcl  9980  djur  9988  djuunxp  9990  eldju2ndl  9993  eldju2ndr  9994  djuun  9995  undjudom  10237  endjudisj  10238  djuen  10239  dju1dif  10242  dju1p1e2  10243  xp2dju  10246  djucomen  10247  djuassen  10248  xpdjuen  10249  mapdjuen  10250  djudom1  10252  djuxpdom  10255  djufi  10256  djuinf  10258  infdju1  10259  ficardadju  10269  pwdjudom  10284  isfin4p1  10384  alephadd  10646  canthp1lem2  10722