![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE 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 5414 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 2, 5 | wf1o 5412 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
8 | vx |
. . . . . . . 8
![]() ![]() | |
9 | 8 | cv 1648 |
. . . . . . 7
![]() ![]() |
10 | vy |
. . . . . . . 8
![]() ![]() | |
11 | 10 | cv 1648 |
. . . . . . 7
![]() ![]() |
12 | 9, 11, 3 | wbr 4172 |
. . . . . 6
![]() ![]() ![]() ![]() |
13 | 9, 5 | cfv 5413 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
14 | 11, 5 | cfv 5413 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
15 | 13, 14, 4 | wbr 4172 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 12, 15 | wb 177 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16, 10, 1 | wral 2666 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 17, 8, 1 | wral 2666 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 7, 18 | wa 359 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 6, 19 | wb 177 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: isoeq1 5998 isoeq2 5999 isoeq3 6000 isoeq4 6001 isoeq5 6002 nfiso 6003 isof1o 6004 isorel 6005 soisores 6006 soisoi 6007 isoid 6008 isocnv 6009 isocnv2 6010 isocnv3 6011 isores2 6012 isores3 6014 isotr 6015 isoini2 6018 f1oiso 6030 f1owe 6032 smoiso2 6590 alephiso 7935 compssiso 8210 negiso 9940 om2uzisoi 11249 icopnfhmeo 18921 reefiso 20317 logltb 20447 isoun 24042 xrmulc1cn 24269 wepwsolem 27006 iso0 27404 |
Copyright terms: Public domain | W3C validator |