Theorem cnveqi 5838

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

Syntax hints:   = wceq 1540  ^◡ccnv 5637

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 3931  df-br 5108  df-opab 5170  df-cnv 5646

This theorem is referenced by:  mptcnv  6112  cnvin  6117  cnvxp  6130  xp0  6131  imainrect  6154  cnvcnv  6165  cnvrescnv  6168  mptpreima  6211  co01  6234  coi2  6236  funcnvpr  6578  funcnvtp  6579  fcoi1  6734  f1oprswap  6844  f1ocnvd  7640  resf1extb  7910  f1iun  7922  mptcnfimad  7965  cnvoprab  8039  fparlem3  8093  fparlem4  8094  tz7.48-2  8410  mapsncnv  8866  sbthlem8  9058  1sdomOLD  9196  cnvepnep  9561  infxpenc2  9975  compsscnv  10324  zorn2lem4  10452  funcnvs1  14878  fsumcom2  15740  fprodcom2  15950  fthoppc  17887  oduval  18249  oduleval  18250  pjdm  21616  qtopres  23585  xkocnv  23701  ustneism  24111  mbfres  25545  dflog2  26469  dfrelog  26474  dvlog  26560  efopnlem2  26566  axcontlem2  28892  2trld  29868  0pth  30054  1pthdlem1  30064  1trld  30071  3trld  30101  ex-cnv  30366  cnvadj  31821  cnvprop  32619  gtiso  32624  padct  32643  f1od2  32644  elrgspnsubrunlem2  33199  ordtcnvNEW  33910  ordtrest2NEW  33913  mbfmcst  34250  0rrv  34442  ballotlemrinv  34525  mthmpps  35569  pprodcnveq  35871  br1cnvres  38258  brcnvrabga  38324  dfxrn2  38358  xrninxp  38378  prjspeclsp  42600  cytpval  43191  resnonrel  43581  cononrel1  43583  cononrel2  43584  cnvtrrel  43659  clsneicnv  44094  neicvgnvo  44104  upgrimpthslem1  47907  tposrescnv  48867