![]() |
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 5218 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 2, 5 | wf1o 5216 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
8 | vx |
. . . . . . . 8
![]() ![]() | |
9 | 8 | cv 1352 |
. . . . . . 7
![]() ![]() |
10 | vy |
. . . . . . . 8
![]() ![]() | |
11 | 10 | cv 1352 |
. . . . . . 7
![]() ![]() |
12 | 9, 11, 3 | wbr 4004 |
. . . . . 6
![]() ![]() ![]() ![]() |
13 | 9, 5 | cfv 5217 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
14 | 11, 5 | cfv 5217 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
15 | 13, 14, 4 | wbr 4004 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 12, 15 | wb 105 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16, 10, 1 | wral 2455 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 17, 8, 1 | wral 2455 |
. . 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 5802 isoeq2 5803 isoeq3 5804 isoeq4 5805 isoeq5 5806 nfiso 5807 isof1o 5808 isorel 5809 isoid 5811 isocnv 5812 isocnv2 5813 isores2 5814 isores3 5816 isotr 5817 iso0 5818 isoini2 5820 f1oiso 5827 negiso 8912 frec2uzisod 10407 zfz1isolem1 10820 xrnegiso 11270 reefiso 14201 logltb 14298 |
Copyright terms: Public domain | W3C validator |