Definition df-dju 9789

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 9786	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4278	. . . . 5 class ∅
5	4	csn 4571	. . . 4 class {∅}
6	5, 1	cxp 5609	. . 3 class ({∅} × 𝐴)
7		c1o 8373	. . . . 5 class 1o
8	7	csn 4571	. . . 4 class {1o}
9	8, 2	cxp 5609	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3895	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1541	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9792  nfdju  9795  djuex  9796  djuexb  9797  djulcl  9798  djurcl  9799  djur  9807  djuunxp  9809  eldju2ndl  9812  eldju2ndr  9813  djuun  9814  undjudom  10054  endjudisj  10055  djuen  10056  dju1dif  10059  dju1p1e2  10060  xp2dju  10063  djucomen  10064  djuassen  10065  xpdjuen  10066  mapdjuen  10067  djudom1  10069  djuxpdom  10072  djufi  10073  djuinf  10075  infdju1  10076  ficardadju  10086  pwdjudom  10101  isfin4p1  10201  alephadd  10463  canthp1lem2  10539