Theorem cnveqi 5859

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

This proof depends on syntax axioms:   = wceq 1569  ^◡ccnv 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921  df-br 5109  df-opab 5173  df-cnv 5668

This theorem is used by:  mptcnv  6137  cnvin  6140  cnvxp  6153  xp0OLD  6154  imainrect  6178  cnvcnv  6189  cnvrescnv  6193  mptpreima  6238  co01  6262  coi2  6264  funcnvpr  6598  funcnvtp  6599  fcoi1  6752  f1oprswap  6866  f1ocnvd  7663  resf1extb  7929  f1iun  7939  mptcnfimad  7981  cnvoprab  8055  fparlem3  8107  fparlem4  8108  tz7.48-2  8427  mapsncnv  8889  sbthlem8  9080  cnvepnep  9575  infxpenc2  10013  compsscnv  10361  zorn2lem4  10489  funcnvs1  14956  fsumcom2  15832  fprodcom2  16045  fthoppc  17988  oduval  18350  oduleval  18351  pjdm  21868  qtopres  23866  xkocnv  23982  ustneism  24392  mbfres  25814  dflog2  26736  dfrelog  26741  dvlog  26827  efopnlem2  26833  axcontlem2  29326  2trld  30298  0pth  30487  1pthdlem1  30497  1trld  30504  3trld  30534  ex-cnv  30799  cnvadj  32255  cnvprop  33052  gtiso  33057  padct  33074  f1od2  33075  elrgspnsubrunlem2  33577  ordtcnvNEW  34319  ordtrest2NEW  34322  mbfmcst  34658  0rrv  34850  ballotlemrinv  34933  mthmpps  36082  pprodcnveq  36381  vxp  38940  br1cnvres  38951  brcnvrabga  39019  dfxrn2  39062  xrninxp  39092  dfpre4  39157  prjspeclsp  43372  cytpval  43957  resnonrel  44346  cononrel1  44348  cononrel2  44349  cnvtrrel  44424  clsneicnv  44859  neicvgnvo  44869  upgrimpthslem1  48700  tposrescnv  49685