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

Definition df-dju 7067
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 7066 . 2  class  ( A B )
4 c0 3437 . . . . 5  class  (/)
54csn 3607 . . . 4  class  { (/) }
65, 1cxp 4642 . . 3  class  ( {
(/) }  X.  A
)
7 c1o 6434 . . . . 5  class  1o
87csn 3607 . . . 4  class  { 1o }
98, 2cxp 4642 . . 3  class  ( { 1o }  X.  B
)
106, 9cun 3142 . 2  class  ( ( { (/) }  X.  A
)  u.  ( { 1o }  X.  B
) )
113, 10wceq 1364 1  wff  ( A B )  =  ( ( { (/) }  X.  A )  u.  ( { 1o }  X.  B
) )
Colors of variables: wff set class
This definition is referenced by:  djueq12  7068  nfdju  7071  djuex  7072  djuexb  7073  djulclr  7078  djurclr  7079  djulcl  7080  djurcl  7081  djulclb  7084  djuunr  7095  eldju2ndl  7101  eldju2ndr  7102  xp2dju  7244  djucomen  7245  djuassen  7246  xpdjuen  7247  djulclALT  15014  djurclALT  15015
  Copyright terms: Public domain W3C validator