Theorem cnveqi 5822

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

Syntax hints:   = wceq 1542  ^◡ccnv 5622

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ss 3917  df-br 5098  df-opab 5160  df-cnv 5631

This theorem is referenced by:  mptcnv  6095  cnvin  6101  cnvxp  6114  xp0OLD  6115  imainrect  6138  cnvcnv  6149  cnvrescnv  6152  mptpreima  6195  co01  6219  coi2  6221  funcnvpr  6553  funcnvtp  6554  fcoi1  6707  f1oprswap  6818  f1ocnvd  7609  resf1extb  7876  f1iun  7888  mptcnfimad  7930  cnvoprab  8004  fparlem3  8056  fparlem4  8057  tz7.48-2  8373  mapsncnv  8833  sbthlem8  9024  cnvepnep  9519  infxpenc2  9934  compsscnv  10283  zorn2lem4  10411  funcnvs1  14837  fsumcom2  15699  fprodcom2  15909  fthoppc  17851  oduval  18213  oduleval  18214  pjdm  21664  qtopres  23644  xkocnv  23760  ustneism  24170  mbfres  25603  dflog2  26527  dfrelog  26532  dvlog  26618  efopnlem2  26624  axcontlem2  29019  2trld  29992  0pth  30181  1pthdlem1  30191  1trld  30198  3trld  30228  ex-cnv  30493  cnvadj  31948  cnvprop  32754  gtiso  32759  padct  32776  f1od2  32777  elrgspnsubrunlem2  33309  ordtcnvNEW  34056  ordtrest2NEW  34059  mbfmcst  34395  0rrv  34587  ballotlemrinv  34670  mthmpps  35755  pprodcnveq  36054  vxp  38433  br1cnvres  38444  brcnvrabga  38512  dfxrn2  38555  xrninxp  38585  dfpre4  38650  prjspeclsp  42892  cytpval  43481  resnonrel  43870  cononrel1  43872  cononrel2  43873  cnvtrrel  43948  clsneicnv  44383  neicvgnvo  44393  upgrimpthslem1  48190  tposrescnv  49161