Definition df-dju 9368

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 9365	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4227	. . . . 5 class ∅
5	4	csn 4525	. . . 4 class {∅}
6	5, 1	cxp 5525	. . 3 class ({∅} × 𝐴)
7		c1o 8110	. . . . 5 class 1o
8	7	csn 4525	. . . 4 class {1o}
9	8, 2	cxp 5525	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3858	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1538	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9371  nfdju  9374  djuex  9375  djuexb  9376  djulcl  9377  djurcl  9378  djur  9386  djuunxp  9388  eldju2ndl  9391  eldju2ndr  9392  djuun  9393  undjudom  9632  endjudisj  9633  djuen  9634  dju1dif  9637  dju1p1e2  9638  xp2dju  9641  djucomen  9642  djuassen  9643  xpdjuen  9644  mapdjuen  9645  djudom1  9647  djuxpdom  9650  djufi  9651  djuinf  9653  infdju1  9654  ficardadju  9664  pwdjudom  9681  isfin4p1  9780  alephadd  10042  canthp1lem2  10118