ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-dju GIF version

Definition df-dju 6923
Description: Disjoint union of two classes. This is a way of creating a class 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 6922 . 2 class (𝐴𝐵)
4 c0 3363 . . . . 5 class
54csn 3527 . . . 4 class {∅}
65, 1cxp 4537 . . 3 class ({∅} × 𝐴)
7 c1o 6306 . . . . 5 class 1o
87csn 3527 . . . 4 class {1o}
98, 2cxp 4537 . . 3 class ({1o} × 𝐵)
106, 9cun 3069 . 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
113, 10wceq 1331 1 wff (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
Colors of variables: wff set class
This definition is referenced by:  djueq12  6924  nfdju  6927  djuex  6928  djuexb  6929  djulclr  6934  djurclr  6935  djulcl  6936  djurcl  6937  djulclb  6940  djuunr  6951  eldju2ndl  6957  eldju2ndr  6958  xp2dju  7076  djucomen  7077  djuassen  7078  xpdjuen  7079  djulclALT  13067  djurclALT  13068
  Copyright terms: Public domain W3C validator