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 5218 | . 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ◡𝐴 = ◡𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ◡ccnv 5037 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-in 3547 df-ss 3554 df-br 4584 df-opab 4644 df-cnv 5046 |
This theorem is referenced by: mptcnv 5453 cnvin 5459 cnvxp 5470 xp0 5471 imainrect 5494 cnvcnv 5505 mptpreima 5545 co01 5567 coi2 5569 funcnvpr 5864 funcnvtp 5865 fcoi1 5991 f1oprswap 6092 f1ocnvd 6782 fun11iun 7019 fparlem3 7166 fparlem4 7167 tz7.48-2 7424 mapsncnv 7790 sbthlem8 7962 1sdom 8048 infxpenc2 8728 compsscnv 9076 zorn2lem4 9204 funcnvs1 13507 fsumcom2 14347 fsumcom2OLD 14348 fprodcom2 14553 fprodcom2OLD 14554 strlemor1 15796 xpsc 16040 fthoppc 16406 oduval 16953 oduleval 16954 pjdm 19870 qtopres 21311 xkocnv 21427 ustneism 21837 mbfres 23217 dflog2 24111 dfrelog 24116 dvlog 24197 efopnlem2 24203 axcontlem2 25645 0pth 26100 1pthonlem1 26119 constr2spthlem1 26124 2pthlem1 26125 constr3pthlem2 26184 ex-cnv 26686 cnvadj 28135 gtiso 28861 padct 28885 cnvoprab 28886 f1od2 28887 ordtcnvNEW 29294 ordtrest2NEW 29297 mbfmcst 29648 0rrv 29840 ballotlemrinv 29922 mthmpps 30733 pprodcnveq 31160 cytpval 36806 resnonrel 36917 cononrel1 36919 cononrel2 36920 cnvtrrel 36981 clsneicnv 37423 neicvgnvo 37433 2trld 41145 0pth-av 41293 1pthdlem1 41302 1trld 41309 3trld 41339 |
Copyright terms: Public domain | W3C validator |