MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dju Structured version   Visualization version   GIF version

Definition df-dju 9122
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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cdju 9119 . 2 class (𝐴𝐵)
4 c0 4172 . . . . 5 class
54csn 4435 . . . 4 class {∅}
65, 1cxp 5401 . . 3 class ({∅} × 𝐴)
7 c1o 7896 . . . . 5 class 1o
87csn 4435 . . . 4 class {1o}
98, 2cxp 5401 . . 3 class ({1o} × 𝐵)
106, 9cun 3820 . 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
113, 10wceq 1508 1 wff (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  djueq12  9125  nfdju  9128  djuex  9129  djuexb  9130  djulcl  9131  djurcl  9132  djur  9140  djuunxp  9142  eldju2ndl  9145  eldju2ndr  9146  djuun  9147  cdadju  9388  undjudom  9389  endjudisj  9390  djuen  9391  dju1dif  9394  dju1p1e2  9395  xp2dju  9398  djucomen  9399  djuassen  9400  xpdjuen  9401  mapdjuen  9402  djudom1  9404  djuxpdom  9407  djufi  9408  djuinf  9410  infdju1  9411  pwdjudom  9434  isfin4p1  9533  alephadd  9795  canthp1lem2  9871
  Copyright terms: Public domain W3C validator