Definition df-dju 9565

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 9562	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4254	. . . . 5 class ∅
5	4	csn 4558	. . . 4 class {∅}
6	5, 1	cxp 5577	. . 3 class ({∅} × 𝐴)
7		c1o 8237	. . . . 5 class 1o
8	7	csn 4558	. . . 4 class {1o}
9	8, 2	cxp 5577	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3882	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1543	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9568  nfdju  9571  djuex  9572  djuexb  9573  djulcl  9574  djurcl  9575  djur  9583  djuunxp  9585  eldju2ndl  9588  eldju2ndr  9589  djuun  9590  undjudom  9829  endjudisj  9830  djuen  9831  dju1dif  9834  dju1p1e2  9835  xp2dju  9838  djucomen  9839  djuassen  9840  xpdjuen  9841  mapdjuen  9842  djudom1  9844  djuxpdom  9847  djufi  9848  djuinf  9850  infdju1  9851  ficardadju  9861  pwdjudom  9878  isfin4p1  9977  alephadd  10239  canthp1lem2  10315