Definition df-dju 9982

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 9979	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4279	. . . . 5 class ∅
5	4	csn 4584	. . . 4 class {∅}
6	5, 1	cxp 5649	. . 3 class ({∅} × 𝐴)
7		c1o 8469	. . . . 5 class 1o
8	7	csn 4584	. . . 4 class {1o}
9	8, 2	cxp 5649	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3897	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1570	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is used by:  djueq12  9985  nfdju  9988  djuex  9989  djuexb  9990  djulcl  9991  djurcl  9992  djur  10000  djuunxp  10002  eldju2ndl  10005  eldju2ndr  10006  djuun  10007  undjudom  10246  endjudisj  10247  djuen  10248  dju1dif  10251  dju1p1e2  10252  xp2dju  10255  djucomen  10256  djuassen  10257  xpdjuen  10258  mapdjuen  10259  djudom1  10261  djuxpdom  10264  djufi  10265  djuinf  10267  infdju1  10268  ficardadju  10278  pwdjudom  10293  isfin4p1  10393  alephadd  10662  canthp1lem2  10738