Theorem cnveqi 5827

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

Syntax hints:   = wceq 1542  ^◡ccnv 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-br 5087  df-opab 5149  df-cnv 5636

This theorem is referenced by:  mptcnv  6100  cnvin  6106  cnvxp  6119  xp0OLD  6120  imainrect  6143  cnvcnv  6154  cnvrescnv  6157  mptpreima  6200  co01  6224  coi2  6226  funcnvpr  6558  funcnvtp  6559  fcoi1  6712  f1oprswap  6823  f1ocnvd  7615  resf1extb  7882  f1iun  7894  mptcnfimad  7936  cnvoprab  8010  fparlem3  8061  fparlem4  8062  tz7.48-2  8378  mapsncnv  8838  sbthlem8  9029  cnvepnep  9526  infxpenc2  9941  compsscnv  10290  zorn2lem4  10418  funcnvs1  14871  fsumcom2  15733  fprodcom2  15946  fthoppc  17889  oduval  18251  oduleval  18252  pjdm  21703  qtopres  23679  xkocnv  23795  ustneism  24205  mbfres  25627  dflog2  26543  dfrelog  26548  dvlog  26634  efopnlem2  26640  axcontlem2  29054  2trld  30027  0pth  30216  1pthdlem1  30226  1trld  30233  3trld  30263  ex-cnv  30528  cnvadj  31984  cnvprop  32790  gtiso  32795  padct  32812  f1od2  32813  elrgspnsubrunlem2  33330  ordtcnvNEW  34086  ordtrest2NEW  34089  mbfmcst  34425  0rrv  34617  ballotlemrinv  34700  mthmpps  35786  pprodcnveq  36085  vxp  38606  br1cnvres  38617  brcnvrabga  38685  dfxrn2  38728  xrninxp  38758  dfpre4  38823  prjspeclsp  43067  cytpval  43656  resnonrel  44045  cononrel1  44047  cononrel2  44048  cnvtrrel  44123  clsneicnv  44558  neicvgnvo  44568  upgrimpthslem1  48403  tposrescnv  49374