Theorem cnveqi 5864

Description: Equality inference for converse relation. (Contributed by NM, 23-Dec-2008.)

Hypothesis

Ref	Expression
cnveqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
cnveqi	⊢ ◡𝐴 = ◡𝐵

Proof of Theorem cnveqi

Step	Hyp	Ref	Expression
1		cnveqi.1	. 2 ⊢ 𝐴 = 𝐵
2		cnveq 5863	. 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
3	1, 2	ax-mp 5	1 ⊢ ◡𝐴 = ◡𝐵

Syntax hints:   = wceq 1568  ^◡ccnv 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-ss 3930  df-br 5115  df-opab 5179  df-cnv 5673

This theorem is referenced by:  mptcnv  6142  cnvin  6145  cnvxp  6158  xp0OLD  6159  imainrect  6183  cnvcnv  6194  cnvrescnv  6198  mptpreima  6243  co01  6267  coi2  6269  funcnvpr  6602  funcnvtp  6603  fcoi1  6756  f1oprswap  6870  f1ocnvd  7665  resf1extb  7934  f1iun  7944  mptcnfimad  7986  cnvoprab  8060  fparlem3  8112  fparlem4  8113  tz7.48-2  8432  mapsncnv  8894  sbthlem8  9085  cnvepnep  9580  infxpenc2  10009  compsscnv  10358  zorn2lem4  10486  funcnvs1  14952  fsumcom2  15828  fprodcom2  16041  fthoppc  17985  oduval  18347  oduleval  18348  pjdm  21840  qtopres  23838  xkocnv  23954  ustneism  24364  mbfres  25786  dflog2  26705  dfrelog  26710  dvlog  26796  efopnlem2  26802  axcontlem2  29285  2trld  30257  0pth  30446  1pthdlem1  30456  1trld  30463  3trld  30493  ex-cnv  30758  cnvadj  32214  cnvprop  33011  gtiso  33016  padct  33033  f1od2  33034  elrgspnsubrunlem2  33538  ordtcnvNEW  34280  ordtrest2NEW  34283  mbfmcst  34619  0rrv  34811  ballotlemrinv  34894  mthmpps  36032  pprodcnveq  36331  vxp  38862  br1cnvres  38873  brcnvrabga  38941  dfxrn2  38984  xrninxp  39014  dfpre4  39079  prjspeclsp  43296  cytpval  43881  resnonrel  44270  cononrel1  44272  cononrel2  44273  cnvtrrel  44348  clsneicnv  44783  neicvgnvo  44793  upgrimpthslem1  48621  tposrescnv  49606