Theorem cnveqi 5841

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

Syntax hints:   = wceq 1540  ^◡ccnv 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-cnv 5649

This theorem is referenced by:  mptcnv  6115  cnvin  6120  cnvxp  6133  xp0  6134  imainrect  6157  cnvcnv  6168  cnvrescnv  6171  mptpreima  6214  co01  6237  coi2  6239  funcnvpr  6581  funcnvtp  6582  fcoi1  6737  f1oprswap  6847  f1ocnvd  7643  resf1extb  7913  f1iun  7925  mptcnfimad  7968  cnvoprab  8042  fparlem3  8096  fparlem4  8097  tz7.48-2  8413  mapsncnv  8869  sbthlem8  9064  1sdomOLD  9203  cnvepnep  9568  infxpenc2  9982  compsscnv  10331  zorn2lem4  10459  funcnvs1  14885  fsumcom2  15747  fprodcom2  15957  fthoppc  17894  oduval  18256  oduleval  18257  pjdm  21623  qtopres  23592  xkocnv  23708  ustneism  24118  mbfres  25552  dflog2  26476  dfrelog  26481  dvlog  26567  efopnlem2  26573  axcontlem2  28899  2trld  29875  0pth  30061  1pthdlem1  30071  1trld  30078  3trld  30108  ex-cnv  30373  cnvadj  31828  cnvprop  32626  gtiso  32631  padct  32650  f1od2  32651  elrgspnsubrunlem2  33206  ordtcnvNEW  33917  ordtrest2NEW  33920  mbfmcst  34257  0rrv  34449  ballotlemrinv  34532  mthmpps  35576  pprodcnveq  35878  br1cnvres  38265  brcnvrabga  38331  dfxrn2  38365  xrninxp  38385  prjspeclsp  42607  cytpval  43198  resnonrel  43588  cononrel1  43590  cononrel2  43591  cnvtrrel  43666  clsneicnv  44101  neicvgnvo  44111  upgrimpthslem1  47911  tposrescnv  48871