Definition df-dju 9805

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 9802	. 2 class (𝐴 ⊔ 𝐵)
4		c0 4282	. . . . 5 class ∅
5	4	csn 4577	. . . 4 class {∅}
6	5, 1	cxp 5619	. . 3 class ({∅} × 𝐴)
7		c1o 8387	. . . . 5 class 1o
8	7	csn 4577	. . . 4 class {1o}
9	8, 2	cxp 5619	. . 3 class ({1o} × 𝐵)
10	6, 9	cun 3896	. 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11	3, 10	wceq 1541	1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))

This definition is referenced by:  djueq12  9808  nfdju  9811  djuex  9812  djuexb  9813  djulcl  9814  djurcl  9815  djur  9823  djuunxp  9825  eldju2ndl  9828  eldju2ndr  9829  djuun  9830  undjudom  10070  endjudisj  10071  djuen  10072  dju1dif  10075  dju1p1e2  10076  xp2dju  10079  djucomen  10080  djuassen  10081  xpdjuen  10082  mapdjuen  10083  djudom1  10085  djuxpdom  10088  djufi  10089  djuinf  10091  infdju1  10092  ficardadju  10102  pwdjudom  10117  isfin4p1  10217  alephadd  10479  canthp1lem2  10555