Theorem cnveqi 5854

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

Syntax hints:   = wceq 1540  ^◡ccnv 5653

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-br 5120  df-opab 5182  df-cnv 5662

This theorem is referenced by:  mptcnv  6128  cnvin  6133  cnvxp  6146  xp0  6147  imainrect  6170  cnvcnv  6181  cnvrescnv  6184  mptpreima  6227  co01  6250  coi2  6252  funcnvpr  6597  funcnvtp  6598  fcoi1  6751  f1oprswap  6861  f1ocnvd  7656  resf1extb  7928  f1iun  7940  mptcnfimad  7983  cnvoprab  8057  fparlem3  8111  fparlem4  8112  tz7.48-2  8454  mapsncnv  8905  sbthlem8  9102  1sdomOLD  9255  cnvepnep  9620  infxpenc2  10034  compsscnv  10383  zorn2lem4  10511  funcnvs1  14929  fsumcom2  15788  fprodcom2  15998  fthoppc  17936  oduval  18298  oduleval  18299  pjdm  21665  qtopres  23634  xkocnv  23750  ustneism  24160  mbfres  25595  dflog2  26519  dfrelog  26524  dvlog  26610  efopnlem2  26616  axcontlem2  28890  2trld  29866  0pth  30052  1pthdlem1  30062  1trld  30069  3trld  30099  ex-cnv  30364  cnvadj  31819  cnvprop  32619  gtiso  32624  padct  32643  f1od2  32644  elrgspnsubrunlem2  33189  ordtcnvNEW  33897  ordtrest2NEW  33900  mbfmcst  34237  0rrv  34429  ballotlemrinv  34512  mthmpps  35550  pprodcnveq  35847  br1cnvres  38233  brcnvrabga  38306  dfxrn2  38340  xrninxp  38356  prjspeclsp  42582  cytpval  43173  resnonrel  43563  cononrel1  43565  cononrel2  43566  cnvtrrel  43641  clsneicnv  44076  neicvgnvo  44086  upgrimpthslem1  47868  tposrescnv  48802