Theorem cnveqi 5819

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

Syntax hints:   = wceq 1548  ^◡ccnv 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ss 3902  df-br 5076  df-opab 5138  df-cnv 5629

This theorem is referenced by:  mptcnv  6096  cnvin  6099  cnvxp  6112  xp0OLD  6113  imainrect  6136  cnvcnv  6147  cnvrescnv  6150  mptpreima  6193  co01  6217  coi2  6219  funcnvpr  6551  funcnvtp  6552  fcoi1  6705  f1oprswap  6816  f1ocnvd  7611  resf1extb  7878  f1iun  7890  mptcnfimad  7932  cnvoprab  8006  fparlem3  8057  fparlem4  8058  tz7.48-2  8375  mapsncnv  8835  sbthlem8  9026  cnvepnep  9524  infxpenc2  9939  compsscnv  10288  zorn2lem4  10416  funcnvs1  14869  fsumcom2  15731  fprodcom2  15944  fthoppc  17887  oduval  18249  oduleval  18250  pjdm  21686  qtopres  23685  xkocnv  23801  ustneism  24211  mbfres  25633  dflog2  26546  dfrelog  26551  dvlog  26637  efopnlem2  26643  axcontlem2  29056  2trld  30028  0pth  30217  1pthdlem1  30227  1trld  30234  3trld  30264  ex-cnv  30529  cnvadj  31985  cnvprop  32792  gtiso  32797  padct  32814  f1od2  32815  elrgspnsubrunlem2  33333  ordtcnvNEW  34116  ordtrest2NEW  34119  mbfmcst  34455  0rrv  34647  ballotlemrinv  34730  mthmpps  35825  pprodcnveq  36124  vxp  38645  br1cnvres  38656  brcnvrabga  38724  dfxrn2  38767  xrninxp  38797  dfpre4  38862  prjspeclsp  43077  cytpval  43662  resnonrel  44051  cononrel1  44053  cononrel2  44054  cnvtrrel  44129  clsneicnv  44564  neicvgnvo  44574  upgrimpthslem1  48412  tposrescnv  49383