![]() |
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 6874 |
. 2
![]() ![]() ![]() ![]() ![]() |
4 | c0 3329 |
. . . . 5
![]() ![]() | |
5 | 4 | csn 3493 |
. . . 4
![]() ![]() ![]() ![]() |
6 | 5, 1 | cxp 4497 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | c1o 6260 |
. . . . 5
![]() ![]() | |
8 | 7 | csn 3493 |
. . . 4
![]() ![]() ![]() ![]() |
9 | 8, 2 | cxp 4497 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 6, 9 | cun 3035 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 3, 10 | wceq 1314 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 |