| 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 5884 | . 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ ◡𝐴 = ◡𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ◡ccnv 5684 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ss 3968 df-br 5144 df-opab 5206 df-cnv 5693 |
| This theorem is referenced by: mptcnv 6159 cnvin 6164 cnvxp 6177 xp0 6178 imainrect 6201 cnvcnv 6212 cnvrescnv 6215 mptpreima 6258 co01 6281 coi2 6283 funcnvpr 6628 funcnvtp 6629 fcoi1 6782 f1oprswap 6892 f1ocnvd 7684 resf1extb 7956 f1iun 7968 mptcnfimad 8011 cnvoprab 8085 fparlem3 8139 fparlem4 8140 tz7.48-2 8482 mapsncnv 8933 sbthlem8 9130 1sdomOLD 9285 cnvepnep 9648 infxpenc2 10062 compsscnv 10411 zorn2lem4 10539 funcnvs1 14951 fsumcom2 15810 fprodcom2 16020 fthoppc 17970 oduval 18333 oduleval 18334 pjdm 21727 qtopres 23706 xkocnv 23822 ustneism 24232 mbfres 25679 dflog2 26602 dfrelog 26607 dvlog 26693 efopnlem2 26699 axcontlem2 28980 2trld 29958 0pth 30144 1pthdlem1 30154 1trld 30161 3trld 30191 ex-cnv 30456 cnvadj 31911 cnvprop 32705 gtiso 32710 padct 32731 f1od2 32732 elrgspnsubrunlem2 33252 ordtcnvNEW 33919 ordtrest2NEW 33922 mbfmcst 34261 0rrv 34453 ballotlemrinv 34536 mthmpps 35587 pprodcnveq 35884 br1cnvres 38270 brcnvrabga 38343 dfxrn2 38377 xrninxp 38393 prjspeclsp 42622 cytpval 43214 resnonrel 43605 cononrel1 43607 cononrel2 43608 cnvtrrel 43683 clsneicnv 44118 neicvgnvo 44128 tposrescnv 48779 |
| Copyright terms: Public domain | W3C validator |