Theorem cnveqi 5719

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

Syntax hints:   = wceq 1538  ^◡ccnv 5526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-br 5036  df-opab 5098  df-cnv 5535

This theorem is referenced by:  mptcnv  5974  cnvin  5979  cnvxp  5990  xp0  5991  imainrect  6014  cnvcnv  6025  cnvrescnv  6028  mptpreima  6071  co01  6095  coi2  6097  funcnvpr  6401  funcnvtp  6402  fcoi1  6541  f1oprswap  6649  f1ocnvd  7397  f1iun  7654  cnvoprab  7767  fparlem3  7819  fparlem4  7820  tz7.48-2  8093  mapsncnv  8480  sbthlem8  8661  1sdom  8764  cnvepnep  9109  infxpenc2  9487  compsscnv  9836  zorn2lem4  9964  funcnvs1  14326  fsumcom2  15182  fprodcom2  15391  fthoppc  17257  oduval  17811  oduleval  17812  pjdm  20477  qtopres  22403  xkocnv  22519  ustneism  22929  mbfres  24349  dflog2  25256  dfrelog  25261  dvlog  25346  efopnlem2  25352  axcontlem2  26863  2trld  27828  0pth  28014  1pthdlem1  28024  1trld  28031  3trld  28061  ex-cnv  28326  cnvadj  29779  cnvprop  30557  gtiso  30561  padct  30582  cnvoprabOLD  30583  f1od2  30584  ordtcnvNEW  31395  ordtrest2NEW  31398  mbfmcst  31749  0rrv  31941  ballotlemrinv  32023  mthmpps  33064  pprodcnveq  33760  brcnvrabga  36065  dfxrn2  36094  xrninxp  36106  prjspeclsp  39976  cytpval  40554  resnonrel  40693  cononrel1  40695  cononrel2  40696  cnvtrrel  40772  clsneicnv  41209  neicvgnvo  41219