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 9892
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 9889 . 2 class (𝐴𝐵)
4 c0 4314 . . . . 5 class
54csn 4620 . . . 4 class {∅}
65, 1cxp 5664 . . 3 class ({∅} × 𝐴)
7 c1o 8454 . . . . 5 class 1o
87csn 4620 . . . 4 class {1o}
98, 2cxp 5664 . . 3 class ({1o} × 𝐵)
106, 9cun 3938 . 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
113, 10wceq 1533 1 wff (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  djueq12  9895  nfdju  9898  djuex  9899  djuexb  9900  djulcl  9901  djurcl  9902  djur  9910  djuunxp  9912  eldju2ndl  9915  eldju2ndr  9916  djuun  9917  undjudom  10158  endjudisj  10159  djuen  10160  dju1dif  10163  dju1p1e2  10164  xp2dju  10167  djucomen  10168  djuassen  10169  xpdjuen  10170  mapdjuen  10171  djudom1  10173  djuxpdom  10176  djufi  10177  djuinf  10179  infdju1  10180  ficardadju  10190  pwdjudom  10207  isfin4p1  10306  alephadd  10568  canthp1lem2  10644
  Copyright terms: Public domain W3C validator