![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-dju | Unicode version |
Description: Disjoint union of two
classes. This is a way of creating a class which
contains elements corresponding to each element of ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-dju |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | 1, 2 | cdju 7066 |
. 2
![]() ![]() ![]() ![]() ![]() |
4 | c0 3437 |
. . . . 5
![]() ![]() | |
5 | 4 | csn 3607 |
. . . 4
![]() ![]() ![]() ![]() |
6 | 5, 1 | cxp 4642 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | c1o 6434 |
. . . . 5
![]() ![]() | |
8 | 7 | csn 3607 |
. . . 4
![]() ![]() ![]() ![]() |
9 | 8, 2 | cxp 4642 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 6, 9 | cun 3142 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 3, 10 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 |