Theorem cnveqi 5823

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

Syntax hints:   = wceq 1541  ^◡ccnv 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-br 5099  df-opab 5161  df-cnv 5632

This theorem is referenced by:  mptcnv  6096  cnvin  6102  cnvxp  6115  xp0OLD  6116  imainrect  6139  cnvcnv  6150  cnvrescnv  6153  mptpreima  6196  co01  6220  coi2  6222  funcnvpr  6554  funcnvtp  6555  fcoi1  6708  f1oprswap  6819  f1ocnvd  7609  resf1extb  7876  f1iun  7888  mptcnfimad  7930  cnvoprab  8004  fparlem3  8056  fparlem4  8057  tz7.48-2  8373  mapsncnv  8831  sbthlem8  9022  cnvepnep  9517  infxpenc2  9932  compsscnv  10281  zorn2lem4  10409  funcnvs1  14835  fsumcom2  15697  fprodcom2  15907  fthoppc  17849  oduval  18211  oduleval  18212  pjdm  21662  qtopres  23642  xkocnv  23758  ustneism  24168  mbfres  25601  dflog2  26525  dfrelog  26530  dvlog  26616  efopnlem2  26622  axcontlem2  29038  2trld  30011  0pth  30200  1pthdlem1  30210  1trld  30217  3trld  30247  ex-cnv  30512  cnvadj  31967  cnvprop  32775  gtiso  32780  padct  32797  f1od2  32798  elrgspnsubrunlem2  33330  ordtcnvNEW  34077  ordtrest2NEW  34080  mbfmcst  34416  0rrv  34608  ballotlemrinv  34691  mthmpps  35776  pprodcnveq  36075  br1cnvres  38467  brcnvrabga  38535  dfxrn2  38570  xrninxp  38600  dfpre4  38654  prjspeclsp  42855  cytpval  43444  resnonrel  43833  cononrel1  43835  cononrel2  43836  cnvtrrel  43911  clsneicnv  44346  neicvgnvo  44356  upgrimpthslem1  48153  tposrescnv  49124