Definition df-dju 9819

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 9816	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4274	. . . . 5 class ∅
5	4	csn 4568	. . . 4 class {∅}
6	5, 1	cxp 5623	. . 3 class ({∅} × 𝐴)
7		c1o 8392	. . . . 5 class 1o
8	7	csn 4568	. . . 4 class {1o}
9	8, 2	cxp 5623	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3888	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1542	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9822  nfdju  9825  djuex  9826  djuexb  9827  djulcl  9828  djurcl  9829  djur  9837  djuunxp  9839  eldju2ndl  9842  eldju2ndr  9843  djuun  9844  undjudom  10084  endjudisj  10085  djuen  10086  dju1dif  10089  dju1p1e2  10090  xp2dju  10093  djucomen  10094  djuassen  10095  xpdjuen  10096  mapdjuen  10097  djudom1  10099  djuxpdom  10102  djufi  10103  djuinf  10105  infdju1  10106  ficardadju  10116  pwdjudom  10131  isfin4p1  10231  alephadd  10494  canthp1lem2  10570