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

Definition df-dju 6875
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 6874 . 2  class  ( A B )
4 c0 3329 . . . . 5  class  (/)
54csn 3493 . . . 4  class  { (/) }
65, 1cxp 4497 . . 3  class  ( {
(/) }  X.  A
)
7 c1o 6260 . . . . 5  class  1o
87csn 3493 . . . 4  class  { 1o }
98, 2cxp 4497 . . 3  class  ( { 1o }  X.  B
)
106, 9cun 3035 . 2  class  ( ( { (/) }  X.  A
)  u.  ( { 1o }  X.  B
) )
113, 10wceq 1314 1  wff  ( A B )  =  ( ( { (/) }  X.  A )  u.  ( { 1o }  X.  B
) )
Colors of variables: wff set class
This definition is referenced by:  djueq12  6876  nfdju  6879  djuex  6880  djuexb  6881  djulclr  6886  djurclr  6887  djulcl  6888  djurcl  6889  djulclb  6892  djuunr  6903  eldju2ndl  6909  eldju2ndr  6910  xp2dju  7019  djucomen  7020  djuassen  7021  xpdjuen  7022  djulclALT  12700  djurclALT  12701
  Copyright terms: Public domain W3C validator