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

Definition df-dju 9368
 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 9365 . 2 class (𝐴𝐵)
4 c0 4227 . . . . 5 class
54csn 4525 . . . 4 class {∅}
65, 1cxp 5525 . . 3 class ({∅} × 𝐴)
7 c1o 8110 . . . . 5 class 1o
87csn 4525 . . . 4 class {1o}
98, 2cxp 5525 . . 3 class ({1o} × 𝐵)
106, 9cun 3858 . 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
113, 10wceq 1538 1 wff (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
 Colors of variables: wff setvar class This definition is referenced by:  djueq12  9371  nfdju  9374  djuex  9375  djuexb  9376  djulcl  9377  djurcl  9378  djur  9386  djuunxp  9388  eldju2ndl  9391  eldju2ndr  9392  djuun  9393  undjudom  9632  endjudisj  9633  djuen  9634  dju1dif  9637  dju1p1e2  9638  xp2dju  9641  djucomen  9642  djuassen  9643  xpdjuen  9644  mapdjuen  9645  djudom1  9647  djuxpdom  9650  djufi  9651  djuinf  9653  infdju1  9654  ficardadju  9664  pwdjudom  9681  isfin4p1  9780  alephadd  10042  canthp1lem2  10118
 Copyright terms: Public domain W3C validator