![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-isom | Unicode version |
Description: Define the isomorphism
predicate. We read this as "![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-isom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | cR |
. . 3
![]() ![]() | |
4 | cS |
. . 3
![]() ![]() | |
5 | cH |
. . 3
![]() ![]() | |
6 | 1, 2, 3, 4, 5 | wiso 5060 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 2, 5 | wf1o 5058 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
8 | vx |
. . . . . . . 8
![]() ![]() | |
9 | 8 | cv 1298 |
. . . . . . 7
![]() ![]() |
10 | vy |
. . . . . . . 8
![]() ![]() | |
11 | 10 | cv 1298 |
. . . . . . 7
![]() ![]() |
12 | 9, 11, 3 | wbr 3875 |
. . . . . 6
![]() ![]() ![]() ![]() |
13 | 9, 5 | cfv 5059 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
14 | 11, 5 | cfv 5059 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
15 | 13, 14, 4 | wbr 3875 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 12, 15 | wb 104 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16, 10, 1 | wral 2375 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 17, 8, 1 | wral 2375 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 7, 18 | wa 103 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 6, 19 | wb 104 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: isoeq1 5634 isoeq2 5635 isoeq3 5636 isoeq4 5637 isoeq5 5638 nfiso 5639 isof1o 5640 isorel 5641 isoid 5643 isocnv 5644 isocnv2 5645 isores2 5646 isores3 5648 isotr 5649 iso0 5650 isoini2 5652 f1oiso 5659 negiso 8571 frec2uzisod 10021 zfz1isolem1 10424 xrnegiso 10870 |
Copyright terms: Public domain | W3C validator |