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

Definition df-dju 7015
Description: Disjoint union of two classes. This is a way of creating a class which contains elements corresponding to each element of  A or  B, tagging each one with whether it came from  A or  B. (Contributed by Jim Kingdon, 20-Jun-2022.)
Assertion
Ref Expression
df-dju  |-  ( A B )  =  ( ( { (/) }  X.  A )  u.  ( { 1o }  X.  B
) )

Detailed syntax breakdown of Definition df-dju
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cdju 7014 . 2  class  ( A B )
4 c0 3414 . . . . 5  class  (/)
54csn 3583 . . . 4  class  { (/) }
65, 1cxp 4609 . . 3  class  ( {
(/) }  X.  A
)
7 c1o 6388 . . . . 5  class  1o
87csn 3583 . . . 4  class  { 1o }
98, 2cxp 4609 . . 3  class  ( { 1o }  X.  B
)
106, 9cun 3119 . 2  class  ( ( { (/) }  X.  A
)  u.  ( { 1o }  X.  B
) )
113, 10wceq 1348 1  wff  ( A B )  =  ( ( { (/) }  X.  A )  u.  ( { 1o }  X.  B
) )
Colors of variables: wff set class
This definition is referenced by:  djueq12  7016  nfdju  7019  djuex  7020  djuexb  7021  djulclr  7026  djurclr  7027  djulcl  7028  djurcl  7029  djulclb  7032  djuunr  7043  eldju2ndl  7049  eldju2ndr  7050  xp2dju  7192  djucomen  7193  djuassen  7194  xpdjuen  7195  djulclALT  13836  djurclALT  13837
  Copyright terms: Public domain W3C validator