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 9941
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 9938 . 2 class (𝐴𝐵)
4 c0 4333 . . . . 5 class
54csn 4626 . . . 4 class {∅}
65, 1cxp 5683 . . 3 class ({∅} × 𝐴)
7 c1o 8499 . . . . 5 class 1o
87csn 4626 . . . 4 class {1o}
98, 2cxp 5683 . . 3 class ({1o} × 𝐵)
106, 9cun 3949 . 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
113, 10wceq 1540 1 wff (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  djueq12  9944  nfdju  9947  djuex  9948  djuexb  9949  djulcl  9950  djurcl  9951  djur  9959  djuunxp  9961  eldju2ndl  9964  eldju2ndr  9965  djuun  9966  undjudom  10208  endjudisj  10209  djuen  10210  dju1dif  10213  dju1p1e2  10214  xp2dju  10217  djucomen  10218  djuassen  10219  xpdjuen  10220  mapdjuen  10221  djudom1  10223  djuxpdom  10226  djufi  10227  djuinf  10229  infdju1  10230  ficardadju  10240  pwdjudom  10255  isfin4p1  10355  alephadd  10617  canthp1lem2  10693
  Copyright terms: Public domain W3C validator