Theorem cnveqi 5813

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

Syntax hints:   = wceq 1541  ^◡ccnv 5613

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914  df-br 5090  df-opab 5152  df-cnv 5622

This theorem is referenced by:  mptcnv  6085  cnvin  6091  cnvxp  6104  xp0OLD  6105  imainrect  6128  cnvcnv  6139  cnvrescnv  6142  mptpreima  6185  co01  6209  coi2  6211  funcnvpr  6543  funcnvtp  6544  fcoi1  6697  f1oprswap  6807  f1ocnvd  7597  resf1extb  7864  f1iun  7876  mptcnfimad  7918  cnvoprab  7992  fparlem3  8044  fparlem4  8045  tz7.48-2  8361  mapsncnv  8817  sbthlem8  9007  cnvepnep  9498  infxpenc2  9913  compsscnv  10262  zorn2lem4  10390  funcnvs1  14819  fsumcom2  15681  fprodcom2  15891  fthoppc  17832  oduval  18194  oduleval  18195  pjdm  21644  qtopres  23613  xkocnv  23729  ustneism  24139  mbfres  25572  dflog2  26496  dfrelog  26501  dvlog  26587  efopnlem2  26593  axcontlem2  28943  2trld  29916  0pth  30105  1pthdlem1  30115  1trld  30122  3trld  30152  ex-cnv  30417  cnvadj  31872  cnvprop  32677  gtiso  32682  padct  32701  f1od2  32702  elrgspnsubrunlem2  33215  ordtcnvNEW  33933  ordtrest2NEW  33936  mbfmcst  34272  0rrv  34464  ballotlemrinv  34547  mthmpps  35626  pprodcnveq  35925  br1cnvres  38305  brcnvrabga  38373  dfxrn2  38408  xrninxp  38438  dfpre4  38492  prjspeclsp  42704  cytpval  43294  resnonrel  43684  cononrel1  43686  cononrel2  43687  cnvtrrel  43762  clsneicnv  44197  neicvgnvo  44207  upgrimpthslem1  48006  tposrescnv  48978