![]() |
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 5229 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 2, 5 | wf1o 5227 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
8 | vx |
. . . . . . . 8
![]() ![]() | |
9 | 8 | cv 1362 |
. . . . . . 7
![]() ![]() |
10 | vy |
. . . . . . . 8
![]() ![]() | |
11 | 10 | cv 1362 |
. . . . . . 7
![]() ![]() |
12 | 9, 11, 3 | wbr 4015 |
. . . . . 6
![]() ![]() ![]() ![]() |
13 | 9, 5 | cfv 5228 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
14 | 11, 5 | cfv 5228 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
15 | 13, 14, 4 | wbr 4015 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 12, 15 | wb 105 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16, 10, 1 | wral 2465 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 17, 8, 1 | wral 2465 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 7, 18 | wa 104 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 6, 19 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: isoeq1 5815 isoeq2 5816 isoeq3 5817 isoeq4 5818 isoeq5 5819 nfiso 5820 isof1o 5821 isorel 5822 isoid 5824 isocnv 5825 isocnv2 5826 isores2 5827 isores3 5829 isotr 5830 iso0 5831 isoini2 5833 f1oiso 5840 negiso 8926 frec2uzisod 10421 zfz1isolem1 10834 xrnegiso 11284 reefiso 14551 logltb 14648 |
Copyright terms: Public domain | W3C validator |