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

Definition df-dju 6873
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 6872 . 2 class (𝐴𝐵)
4 c0 3327 . . . . 5 class
54csn 3491 . . . 4 class {∅}
65, 1cxp 4495 . . 3 class ({∅} × 𝐴)
7 c1o 6258 . . . . 5 class 1o
87csn 3491 . . . 4 class {1o}
98, 2cxp 4495 . . 3 class ({1o} × 𝐵)
106, 9cun 3033 . 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵))
113, 10wceq 1312 1 wff (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
Colors of variables: wff set class
This definition is referenced by:  djueq12  6874  nfdju  6877  djuex  6878  djuexb  6879  djulclr  6884  djurclr  6885  djulcl  6886  djurcl  6887  djulclb  6890  djuunr  6901  eldju2ndl  6907  eldju2ndr  6908  xp2dju  7016  djucomen  7017  djuassen  7018  xpdjuen  7019  djulclALT  12691  djurclALT  12692
  Copyright terms: Public domain W3C validator