![]() |
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 5630 | . 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ◡𝐴 = ◡𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 ◡ccnv 5442 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-in 3866 df-ss 3874 df-br 4963 df-opab 5025 df-cnv 5451 |
This theorem is referenced by: mptcnv 5874 cnvin 5879 cnvxp 5890 xp0 5891 imainrect 5914 cnvcnv 5925 mptpreima 5967 co01 5989 coi2 5991 funcnvpr 6286 funcnvtp 6287 fcoi1 6420 f1oprswap 6526 f1ocnvd 7254 f1iun 7501 cnvoprab 7614 fparlem3 7665 fparlem4 7666 tz7.48-2 7929 mapsncnv 8306 sbthlem8 8481 1sdom 8567 cnvepnep 8917 infxpenc2 9294 compsscnv 9639 zorn2lem4 9767 funcnvs1 14110 fsumcom2 14962 fprodcom2 15171 fthoppc 17022 oduval 17569 oduleval 17570 pjdm 20533 qtopres 21990 xkocnv 22106 ustneism 22515 mbfres 23928 dflog2 24825 dfrelog 24830 dvlog 24915 efopnlem2 24921 axcontlem2 26434 2trld 27404 0pth 27591 1pthdlem1 27601 1trld 27608 3trld 27638 ex-cnv 27908 cnvadj 29360 cnvprop 30120 gtiso 30124 padct 30143 cnvoprabOLD 30144 f1od2 30145 ordtcnvNEW 30780 ordtrest2NEW 30783 mbfmcst 31134 0rrv 31326 ballotlemrinv 31408 mthmpps 32437 pprodcnveq 32953 brcnvrabga 35131 dfxrn2 35159 xrninxp 35171 prjspeclsp 38759 cytpval 39294 resnonrel 39437 cononrel1 39439 cononrel2 39440 cnvtrrel 39500 clsneicnv 39940 neicvgnvo 39950 |
Copyright terms: Public domain | W3C validator |