Theorem cnveqi 5828

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 5827	. 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
3	1, 2	ax-mp 5	1 ⊢ ◡𝐴 = ◡𝐵

Syntax hints:   = wceq 1540  ^◡ccnv 5630

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-br 5103  df-opab 5165  df-cnv 5639

This theorem is referenced by:  mptcnv  6100  cnvin  6105  cnvxp  6118  xp0  6119  imainrect  6142  cnvcnv  6153  cnvrescnv  6156  mptpreima  6199  co01  6222  coi2  6224  funcnvpr  6562  funcnvtp  6563  fcoi1  6716  f1oprswap  6826  f1ocnvd  7620  resf1extb  7890  f1iun  7902  mptcnfimad  7944  cnvoprab  8018  fparlem3  8070  fparlem4  8071  tz7.48-2  8387  mapsncnv  8843  sbthlem8  9035  1sdomOLD  9172  cnvepnep  9537  infxpenc2  9951  compsscnv  10300  zorn2lem4  10428  funcnvs1  14854  fsumcom2  15716  fprodcom2  15926  fthoppc  17867  oduval  18229  oduleval  18230  pjdm  21649  qtopres  23618  xkocnv  23734  ustneism  24144  mbfres  25578  dflog2  26502  dfrelog  26507  dvlog  26593  efopnlem2  26599  axcontlem2  28945  2trld  29918  0pth  30104  1pthdlem1  30114  1trld  30121  3trld  30151  ex-cnv  30416  cnvadj  31871  cnvprop  32669  gtiso  32674  padct  32693  f1od2  32694  elrgspnsubrunlem2  33215  ordtcnvNEW  33903  ordtrest2NEW  33906  mbfmcst  34243  0rrv  34435  ballotlemrinv  34518  mthmpps  35562  pprodcnveq  35864  br1cnvres  38251  brcnvrabga  38317  dfxrn2  38351  xrninxp  38371  prjspeclsp  42593  cytpval  43184  resnonrel  43574  cononrel1  43576  cononrel2  43577  cnvtrrel  43652  clsneicnv  44087  neicvgnvo  44097  upgrimpthslem1  47900  tposrescnv  48860