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. (Contributed by NM, 23-Dec-2008.) |
Ref | Expression |
---|---|
cnveqi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
cnveqi | ⊢ ◡𝐴 = ◡𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnveqi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | cnveq 5296 | . 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ◡𝐴 = ◡𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1483 ◡ccnv 5113 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-in 3581 df-ss 3588 df-br 4654 df-opab 4713 df-cnv 5122 |
This theorem is referenced by: mptcnv 5534 cnvin 5540 cnvxp 5551 xp0 5552 imainrect 5575 cnvcnv 5586 cnvcnvOLD 5587 mptpreima 5628 co01 5650 coi2 5652 funcnvpr 5950 funcnvtp 5951 fcoi1 6078 f1oprswap 6180 f1ocnvd 6884 fun11iun 7126 fparlem3 7279 fparlem4 7280 tz7.48-2 7537 mapsncnv 7904 sbthlem8 8077 1sdom 8163 infxpenc2 8845 compsscnv 9193 zorn2lem4 9321 funcnvs1 13657 fsumcom2 14505 fsumcom2OLD 14506 fprodcom2 14714 fprodcom2OLD 14715 strlemor1OLD 15969 xpsc 16217 fthoppc 16583 oduval 17130 oduleval 17131 pjdm 20051 qtopres 21501 xkocnv 21617 ustneism 22027 mbfres 23411 dflog2 24307 dfrelog 24312 dvlog 24397 efopnlem2 24403 axcontlem2 25845 2trld 26834 0pth 26986 1pthdlem1 26995 1trld 27002 3trld 27032 ex-cnv 27294 cnvadj 28751 gtiso 29478 padct 29497 cnvoprab 29498 f1od2 29499 ordtcnvNEW 29966 ordtrest2NEW 29969 mbfmcst 30321 0rrv 30513 ballotlemrinv 30595 mthmpps 31479 pprodcnveq 31990 cytpval 37787 resnonrel 37898 cononrel1 37900 cononrel2 37901 cnvtrrel 37962 clsneicnv 38403 neicvgnvo 38413 |
Copyright terms: Public domain | W3C validator |