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

Definition df-dju 6731
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 (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵))

Detailed syntax breakdown of Definition df-dju
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cdju 6730 . 2 class (𝐴𝐵)
4 c0 3286 . . . . 5 class
54csn 3446 . . . 4 class {∅}
65, 1cxp 4436 . . 3 class ({∅} × 𝐴)
7 c1o 6174 . . . . 5 class 1𝑜
87csn 3446 . . . 4 class {1𝑜}
98, 2cxp 4436 . . 3 class ({1𝑜} × 𝐵)
106, 9cun 2997 . 2 class (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵))
113, 10wceq 1289 1 wff (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵))
Colors of variables: wff set class
This definition is referenced by:  djueq12  6732  nfdju  6735  djuex  6736  djulclr  6741  djurclr  6742  djulcl  6743  djurcl  6744  djulclb  6747  djur  6757  djuunr  6758  eldju2ndl  6763  eldju2ndr  6764  djulclALT  11701  djurclALT  11702
  Copyright terms: Public domain W3C validator