Theorem cnveqi 5772

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

Syntax hints:   = wceq 1539  ^◡ccnv 5579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071  df-opab 5133  df-cnv 5588

This theorem is referenced by:  mptcnv  6032  cnvin  6037  cnvxp  6049  xp0  6050  imainrect  6073  cnvcnv  6084  cnvrescnv  6087  mptpreima  6130  co01  6154  coi2  6156  funcnvpr  6480  funcnvtp  6481  fcoi1  6632  f1oprswap  6743  f1ocnvd  7498  f1iun  7760  cnvoprab  7873  fparlem3  7925  fparlem4  7926  tz7.48-2  8243  mapsncnv  8639  sbthlem8  8830  1sdom  8955  cnvepnep  9296  infxpenc2  9709  compsscnv  10058  zorn2lem4  10186  funcnvs1  14553  fsumcom2  15414  fprodcom2  15622  fthoppc  17555  oduval  17922  oduleval  17923  pjdm  20824  qtopres  22757  xkocnv  22873  ustneism  23283  mbfres  24713  dflog2  25621  dfrelog  25626  dvlog  25711  efopnlem2  25717  axcontlem2  27236  2trld  28204  0pth  28390  1pthdlem1  28400  1trld  28407  3trld  28437  ex-cnv  28702  cnvadj  30155  cnvprop  30931  gtiso  30935  padct  30956  cnvoprabOLD  30957  f1od2  30958  ordtcnvNEW  31772  ordtrest2NEW  31775  mbfmcst  32126  0rrv  32318  ballotlemrinv  32400  mthmpps  33444  pprodcnveq  34112  brcnvrabga  36404  dfxrn2  36433  xrninxp  36445  prjspeclsp  40372  cytpval  40950  resnonrel  41089  cononrel1  41091  cononrel2  41092  cnvtrrel  41167  clsneicnv  41604  neicvgnvo  41614