Theorem cnveqi 5786

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

Syntax hints:   = wceq 1539  ^◡ccnv 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-br 5076  df-opab 5138  df-cnv 5598

This theorem is referenced by:  mptcnv  6048  cnvin  6053  cnvxp  6065  xp0  6066  imainrect  6089  cnvcnv  6100  cnvrescnv  6103  mptpreima  6146  co01  6169  coi2  6171  funcnvpr  6503  funcnvtp  6504  fcoi1  6657  f1oprswap  6769  f1ocnvd  7529  f1iun  7795  cnvoprab  7909  fparlem3  7963  fparlem4  7964  tz7.48-2  8282  mapsncnv  8690  sbthlem8  8886  1sdom  9034  cnvepnep  9375  infxpenc2  9787  compsscnv  10136  zorn2lem4  10264  funcnvs1  14634  fsumcom2  15495  fprodcom2  15703  fthoppc  17648  oduval  18015  oduleval  18016  pjdm  20923  qtopres  22858  xkocnv  22974  ustneism  23384  mbfres  24817  dflog2  25725  dfrelog  25730  dvlog  25815  efopnlem2  25821  axcontlem2  27342  2trld  28312  0pth  28498  1pthdlem1  28508  1trld  28515  3trld  28545  ex-cnv  28810  cnvadj  30263  cnvprop  31038  gtiso  31042  padct  31063  cnvoprabOLD  31064  f1od2  31065  ordtcnvNEW  31879  ordtrest2NEW  31882  mbfmcst  32235  0rrv  32427  ballotlemrinv  32509  mthmpps  33553  pprodcnveq  34194  brcnvrabga  36484  dfxrn2  36513  xrninxp  36525  prjspeclsp  40458  cytpval  41041  resnonrel  41207  cononrel1  41209  cononrel2  41210  cnvtrrel  41285  clsneicnv  41722  neicvgnvo  41732