Theorem cnveqi 5631

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

Syntax hints:   = wceq 1522  ^◡ccnv 5442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-in 3866  df-ss 3874  df-br 4963  df-opab 5025  df-cnv 5451

This theorem is referenced by:  mptcnv  5874  cnvin  5879  cnvxp  5890  xp0  5891  imainrect  5914  cnvcnv  5925  mptpreima  5967  co01  5989  coi2  5991  funcnvpr  6286  funcnvtp  6287  fcoi1  6420  f1oprswap  6526  f1ocnvd  7254  f1iun  7501  cnvoprab  7614  fparlem3  7665  fparlem4  7666  tz7.48-2  7929  mapsncnv  8306  sbthlem8  8481  1sdom  8567  cnvepnep  8917  infxpenc2  9294  compsscnv  9639  zorn2lem4  9767  funcnvs1  14110  fsumcom2  14962  fprodcom2  15171  fthoppc  17022  oduval  17569  oduleval  17570  pjdm  20533  qtopres  21990  xkocnv  22106  ustneism  22515  mbfres  23928  dflog2  24825  dfrelog  24830  dvlog  24915  efopnlem2  24921  axcontlem2  26434  2trld  27404  0pth  27591  1pthdlem1  27601  1trld  27608  3trld  27638  ex-cnv  27908  cnvadj  29360  cnvprop  30120  gtiso  30124  padct  30143  cnvoprabOLD  30144  f1od2  30145  ordtcnvNEW  30780  ordtrest2NEW  30783  mbfmcst  31134  0rrv  31326  ballotlemrinv  31408  mthmpps  32437  pprodcnveq  32953  brcnvrabga  35131  dfxrn2  35159  xrninxp  35171  prjspeclsp  38759  cytpval  39294  resnonrel  39437  cononrel1  39439  cononrel2  39440  cnvtrrel  39500  clsneicnv  39940  neicvgnvo  39950