Theorem cnveqi 5848

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

Syntax hints:   = wceq 1562  ^◡ccnv 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ss 3923  df-br 5103  df-opab 5165  df-cnv 5657

This theorem is referenced by:  mptcnv  6127  cnvin  6130  cnvxp  6144  xp0OLD  6145  imainrect  6169  cnvcnv  6180  cnvrescnv  6184  mptpreima  6227  co01  6251  coi2  6253  funcnvpr  6585  funcnvtp  6586  fcoi1  6740  f1oprswap  6854  f1ocnvd  7649  resf1extb  7917  f1iun  7927  mptcnfimad  7969  cnvoprab  8043  fparlem3  8095  fparlem4  8096  tz7.48-2  8415  mapsncnv  8877  sbthlem8  9068  cnvepnep  9565  infxpenc2  9980  compsscnv  10330  zorn2lem4  10458  funcnvs1  14927  fsumcom2  15803  fprodcom2  16016  fthoppc  17960  oduval  18322  oduleval  18323  pjdm  21761  qtopres  23760  xkocnv  23876  ustneism  24286  mbfres  25708  dflog2  26627  dfrelog  26632  dvlog  26718  efopnlem2  26724  axcontlem2  29168  2trld  30140  0pth  30329  1pthdlem1  30339  1trld  30346  3trld  30376  ex-cnv  30641  cnvadj  32097  cnvprop  32900  gtiso  32905  padct  32922  f1od2  32923  elrgspnsubrunlem2  33431  ordtcnvNEW  34219  ordtrest2NEW  34222  mbfmcst  34558  0rrv  34750  ballotlemrinv  34833  mthmpps  35937  pprodcnveq  36236  vxp  38767  br1cnvres  38778  brcnvrabga  38846  dfxrn2  38889  xrninxp  38919  dfpre4  38984  prjspeclsp  43199  cytpval  43784  resnonrel  44173  cononrel1  44175  cononrel2  44176  cnvtrrel  44251  clsneicnv  44686  neicvgnvo  44696  upgrimpthslem1  48534  tposrescnv  49505