![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnveq | Structured version Visualization version Unicode version |
Description: Equality theorem for converse. (Contributed by NM, 13-Aug-1995.) |
Ref | Expression |
---|---|
cnveq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvss 4985 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | cnvss 4985 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | anim12i 574 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eqss 3415 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eqss 3415 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3imtr4i 274 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-in 3379 df-ss 3386 df-br 4375 df-opab 4434 df-cnv 4820 |
This theorem is referenced by: cnveqi 4987 cnveqd 4988 rneq 5038 cnveqb 5270 predeq123 5360 f1eq1 5757 f1o00 5830 foeqcnvco 6184 funcnvuni 6734 tposfn2 6982 ereq1 7357 infeq3 7983 1arith 14882 vdwmc 14939 vdwnnlem1 14956 ramub2 14982 rami 14983 isps 16459 istsr 16474 isdir 16489 isrim0 17962 psrbag 18599 psrbaglefi 18607 iscn 20262 ishmeo 20785 symgtgp 21127 ustincl 21233 ustdiag 21234 ustinvel 21235 ustexhalf 21236 ustexsym 21241 ust0 21245 isi1f 22644 itg1val 22653 fta1lem 23272 fta1 23273 vieta1lem2 23276 vieta1 23277 sqff1o 24121 istrl 25279 isspth 25311 0spth 25313 nlfnval 27546 padct 28315 indf1ofs 28854 ismbfm 29080 issibf 29172 sitgfval 29180 eulerpartlemelr 29196 eulerpartleme 29202 eulerpartlemo 29204 eulerpartlemt0 29208 eulerpartlemt 29210 eulerpartgbij 29211 eulerpartlemr 29213 eulerpartlemgs2 29219 eulerpartlemn 29220 eulerpart 29221 iscvm 29988 elmpst 30180 wlimeq12 30508 lkrval 32656 ltrncnvnid 33694 cdlemkuu 34464 pw2f1o2val 35896 pwfi2f1o 35956 clcnvlem 36232 f1ssf1 39115 isTrl 39787 issPth 39810 upgrwlkdvspth 39823 uhgr1wlkspthlem1 39837 0spth-av 39894 isrngisom 40221 |
Copyright terms: Public domain | W3C validator |