Definition df-dju 9813

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 9810	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4285	. . . . 5 class ∅
5	4	csn 4580	. . . 4 class {∅}
6	5, 1	cxp 5622	. . 3 class ({∅} × 𝐴)
7		c1o 8390	. . . . 5 class 1o
8	7	csn 4580	. . . 4 class {1o}
9	8, 2	cxp 5622	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3899	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1541	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9816  nfdju  9819  djuex  9820  djuexb  9821  djulcl  9822  djurcl  9823  djur  9831  djuunxp  9833  eldju2ndl  9836  eldju2ndr  9837  djuun  9838  undjudom  10078  endjudisj  10079  djuen  10080  dju1dif  10083  dju1p1e2  10084  xp2dju  10087  djucomen  10088  djuassen  10089  xpdjuen  10090  mapdjuen  10091  djudom1  10093  djuxpdom  10096  djufi  10097  djuinf  10099  infdju1  10100  ficardadju  10110  pwdjudom  10125  isfin4p1  10225  alephadd  10488  canthp1lem2  10564