Theorem cnveqi 5828

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

Syntax hints:   = wceq 1540  ^◡ccnv 5630

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 3928  df-br 5103  df-opab 5165  df-cnv 5639

This theorem is referenced by:  mptcnv  6100  cnvin  6105  cnvxp  6118  xp0  6119  imainrect  6142  cnvcnv  6153  cnvrescnv  6156  mptpreima  6199  co01  6222  coi2  6224  funcnvpr  6562  funcnvtp  6563  fcoi1  6716  f1oprswap  6826  f1ocnvd  7620  resf1extb  7890  f1iun  7902  mptcnfimad  7944  cnvoprab  8018  fparlem3  8070  fparlem4  8071  tz7.48-2  8387  mapsncnv  8843  sbthlem8  9035  1sdomOLD  9172  cnvepnep  9539  infxpenc2  9953  compsscnv  10302  zorn2lem4  10430  funcnvs1  14855  fsumcom2  15717  fprodcom2  15927  fthoppc  17868  oduval  18230  oduleval  18231  pjdm  21650  qtopres  23619  xkocnv  23735  ustneism  24145  mbfres  25579  dflog2  26503  dfrelog  26508  dvlog  26594  efopnlem2  26600  axcontlem2  28946  2trld  29919  0pth  30105  1pthdlem1  30115  1trld  30122  3trld  30152  ex-cnv  30417  cnvadj  31872  cnvprop  32670  gtiso  32675  padct  32694  f1od2  32695  elrgspnsubrunlem2  33216  ordtcnvNEW  33904  ordtrest2NEW  33907  mbfmcst  34244  0rrv  34436  ballotlemrinv  34519  mthmpps  35563  pprodcnveq  35865  br1cnvres  38252  brcnvrabga  38318  dfxrn2  38352  xrninxp  38372  prjspeclsp  42594  cytpval  43185  resnonrel  43575  cononrel1  43577  cononrel2  43578  cnvtrrel  43653  clsneicnv  44088  neicvgnvo  44098  upgrimpthslem1  47901  tposrescnv  48861