![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnveqi | Structured version Visualization version Unicode version |
Description: Equality inference for converse. (Contributed by NM, 23-Dec-2008.) |
Ref | Expression |
---|---|
cnveqi.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
cnveqi |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnveqi.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | cnveq 5027 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-in 3423 df-ss 3430 df-br 4417 df-opab 4476 df-cnv 4861 |
This theorem is referenced by: mptcnv 5257 cnvin 5262 cnvxp 5273 xp0 5274 imainrect 5297 cnvcnv 5307 mptpreima 5347 co01 5369 coi2 5371 funcnvpr 5658 funcnvtp 5659 fcoi1 5780 f1oprswap 5877 f1ocnvd 6545 fun11iun 6780 fparlem3 6925 fparlem4 6926 tz7.48-2 7185 mapsncnv 7544 sbthlem8 7715 1sdom 7801 infxpenc2 8479 compsscnv 8827 zorn2lem4 8955 funcnvs1 13043 fsumcom2 13884 fprodcom2 14087 strlemor1 15266 xpsc 15512 fthoppc 15877 oduval 16425 oduleval 16426 pjdm 19319 qtopres 20762 xkocnv 20878 ustneism 21287 mbfres 22649 dflog2 23559 dfrelog 23564 dvlog 23645 efopnlem2 23651 axcontlem2 25044 0pth 25349 1pthonlem1 25368 constr2spthlem1 25373 2pthlem1 25374 constr3pthlem2 25433 ex-cnv 25936 cnvadj 27594 gtiso 28330 padct 28356 cnvoprab 28357 f1od2 28358 ordtcnvNEW 28775 ordtrest2NEW 28778 mbfmcst 29130 0rrv 29333 ballotlemrinv 29415 ballotlemrinvOLD 29453 mthmpps 30269 pprodcnveq 30699 cytpval 36131 resnonrel 36243 cononrel1 36245 cononrel2 36246 cnvtrrel 36307 0pth-av 39841 1pthdlem1 39850 1trld 39857 2trld 39887 3trld 39913 |
Copyright terms: Public domain | W3C validator |