Definition df-dju 9892

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 9889	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4314	. . . . 5 class ∅
5	4	csn 4620	. . . 4 class {∅}
6	5, 1	cxp 5664	. . 3 class ({∅} × 𝐴)
7		c1o 8454	. . . . 5 class 1o
8	7	csn 4620	. . . 4 class {1o}
9	8, 2	cxp 5664	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3938	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1533	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9895  nfdju  9898  djuex  9899  djuexb  9900  djulcl  9901  djurcl  9902  djur  9910  djuunxp  9912  eldju2ndl  9915  eldju2ndr  9916  djuun  9917  undjudom  10158  endjudisj  10159  djuen  10160  dju1dif  10163  dju1p1e2  10164  xp2dju  10167  djucomen  10168  djuassen  10169  xpdjuen  10170  mapdjuen  10171  djudom1  10173  djuxpdom  10176  djufi  10177  djuinf  10179  infdju1  10180  ficardadju  10190  pwdjudom  10207  isfin4p1  10306  alephadd  10568  canthp1lem2  10644