Theorem cnveqi 5864

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

Syntax hints:   = wceq 1533  ^◡ccnv 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957  df-br 5139  df-opab 5201  df-cnv 5674

This theorem is referenced by:  mptcnv  6129  cnvin  6134  cnvxp  6146  xp0  6147  imainrect  6170  cnvcnv  6181  cnvrescnv  6184  mptpreima  6227  co01  6250  coi2  6252  funcnvpr  6600  funcnvtp  6601  fcoi1  6755  f1oprswap  6867  f1ocnvd  7650  f1iun  7923  cnvoprab  8039  fparlem3  8094  fparlem4  8095  tz7.48-2  8437  mapsncnv  8882  sbthlem8  9085  1sdomOLD  9244  cnvepnep  9598  infxpenc2  10012  compsscnv  10361  zorn2lem4  10489  funcnvs1  14859  fsumcom2  15716  fprodcom2  15924  fthoppc  17872  oduval  18240  oduleval  18241  pjdm  21562  qtopres  23512  xkocnv  23628  ustneism  24038  mbfres  25483  dflog2  26399  dfrelog  26404  dvlog  26489  efopnlem2  26495  axcontlem2  28647  2trld  29616  0pth  29802  1pthdlem1  29812  1trld  29819  3trld  29849  ex-cnv  30114  cnvadj  31569  cnvprop  32342  gtiso  32346  padct  32368  cnvoprabOLD  32369  f1od2  32370  ordtcnvNEW  33355  ordtrest2NEW  33358  mbfmcst  33713  0rrv  33905  ballotlemrinv  33987  mthmpps  35028  pprodcnveq  35316  br1cnvres  37593  brcnvrabga  37667  dfxrn2  37702  xrninxp  37718  prjspeclsp  41809  cytpval  42406  resnonrel  42798  cononrel1  42800  cononrel2  42801  cnvtrrel  42876  clsneicnv  43311  neicvgnvo  43321