![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnveqi | Structured version Visualization version GIF version |
Description: Equality inference for converse relation. (Contributed by NM, 23-Dec-2008.) |
Ref | Expression |
---|---|
cnveqi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
cnveqi | ⊢ ◡𝐴 = ◡𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnveqi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | cnveq 5863 | . 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ◡𝐴 = ◡𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ◡ccnv 5665 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-v 3468 df-in 3947 df-ss 3957 df-br 5139 df-opab 5201 df-cnv 5674 |
This theorem is referenced by: mptcnv 6129 cnvin 6134 cnvxp 6146 xp0 6147 imainrect 6170 cnvcnv 6181 cnvrescnv 6184 mptpreima 6227 co01 6250 coi2 6252 funcnvpr 6600 funcnvtp 6601 fcoi1 6755 f1oprswap 6867 f1ocnvd 7650 f1iun 7923 cnvoprab 8039 fparlem3 8094 fparlem4 8095 tz7.48-2 8437 mapsncnv 8882 sbthlem8 9085 1sdomOLD 9244 cnvepnep 9598 infxpenc2 10012 compsscnv 10361 zorn2lem4 10489 funcnvs1 14859 fsumcom2 15716 fprodcom2 15924 fthoppc 17872 oduval 18240 oduleval 18241 pjdm 21562 qtopres 23512 xkocnv 23628 ustneism 24038 mbfres 25483 dflog2 26399 dfrelog 26404 dvlog 26489 efopnlem2 26495 axcontlem2 28647 2trld 29616 0pth 29802 1pthdlem1 29812 1trld 29819 3trld 29849 ex-cnv 30114 cnvadj 31569 cnvprop 32342 gtiso 32346 padct 32368 cnvoprabOLD 32369 f1od2 32370 ordtcnvNEW 33355 ordtrest2NEW 33358 mbfmcst 33713 0rrv 33905 ballotlemrinv 33987 mthmpps 35028 pprodcnveq 35316 br1cnvres 37593 brcnvrabga 37667 dfxrn2 37702 xrninxp 37718 prjspeclsp 41809 cytpval 42406 resnonrel 42798 cononrel1 42800 cononrel2 42801 cnvtrrel 42876 clsneicnv 43311 neicvgnvo 43321 |
Copyright terms: Public domain | W3C validator |