Theorem cnveqi 5833

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

Syntax hints:   = wceq 1542  ^◡ccnv 5633

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 3920  df-br 5101  df-opab 5163  df-cnv 5642

This theorem is referenced by:  mptcnv  6106  cnvin  6112  cnvxp  6125  xp0OLD  6126  imainrect  6149  cnvcnv  6160  cnvrescnv  6163  mptpreima  6206  co01  6230  coi2  6232  funcnvpr  6564  funcnvtp  6565  fcoi1  6718  f1oprswap  6829  f1ocnvd  7621  resf1extb  7888  f1iun  7900  mptcnfimad  7942  cnvoprab  8016  fparlem3  8068  fparlem4  8069  tz7.48-2  8385  mapsncnv  8845  sbthlem8  9036  cnvepnep  9531  infxpenc2  9946  compsscnv  10295  zorn2lem4  10423  funcnvs1  14849  fsumcom2  15711  fprodcom2  15921  fthoppc  17863  oduval  18225  oduleval  18226  pjdm  21679  qtopres  23659  xkocnv  23775  ustneism  24185  mbfres  25618  dflog2  26542  dfrelog  26547  dvlog  26633  efopnlem2  26639  axcontlem2  29056  2trld  30029  0pth  30218  1pthdlem1  30228  1trld  30235  3trld  30265  ex-cnv  30530  cnvadj  31986  cnvprop  32792  gtiso  32797  padct  32814  f1od2  32815  elrgspnsubrunlem2  33348  ordtcnvNEW  34104  ordtrest2NEW  34107  mbfmcst  34443  0rrv  34635  ballotlemrinv  34718  mthmpps  35804  pprodcnveq  36103  vxp  38543  br1cnvres  38554  brcnvrabga  38622  dfxrn2  38665  xrninxp  38695  dfpre4  38760  prjspeclsp  42999  cytpval  43588  resnonrel  43977  cononrel1  43979  cononrel2  43980  cnvtrrel  44055  clsneicnv  44490  neicvgnvo  44500  upgrimpthslem1  48296  tposrescnv  49267