Theorem cnveqi 5887

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

Syntax hints:   = wceq 1536  ^◡ccnv 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-br 5148  df-opab 5210  df-cnv 5696

This theorem is referenced by:  mptcnv  6161  cnvin  6166  cnvxp  6178  xp0  6179  imainrect  6202  cnvcnv  6213  cnvrescnv  6216  mptpreima  6259  co01  6282  coi2  6284  funcnvpr  6629  funcnvtp  6630  fcoi1  6782  f1oprswap  6892  f1ocnvd  7683  f1iun  7966  mptcnfimad  8009  cnvoprab  8083  fparlem3  8137  fparlem4  8138  tz7.48-2  8480  mapsncnv  8931  sbthlem8  9128  1sdomOLD  9282  cnvepnep  9645  infxpenc2  10059  compsscnv  10408  zorn2lem4  10536  funcnvs1  14947  fsumcom2  15806  fprodcom2  16016  fthoppc  17976  oduval  18344  oduleval  18345  pjdm  21744  qtopres  23721  xkocnv  23837  ustneism  24247  mbfres  25692  dflog2  26616  dfrelog  26621  dvlog  26707  efopnlem2  26713  axcontlem2  28994  2trld  29967  0pth  30153  1pthdlem1  30163  1trld  30170  3trld  30200  ex-cnv  30465  cnvadj  31920  cnvprop  32710  gtiso  32715  padct  32736  cnvoprabOLD  32737  f1od2  32738  ordtcnvNEW  33880  ordtrest2NEW  33883  mbfmcst  34240  0rrv  34432  ballotlemrinv  34514  mthmpps  35566  pprodcnveq  35864  br1cnvres  38250  brcnvrabga  38323  dfxrn2  38357  xrninxp  38373  prjspeclsp  42598  cytpval  43190  resnonrel  43581  cononrel1  43583  cononrel2  43584  cnvtrrel  43659  clsneicnv  44094  neicvgnvo  44104