Theorem cnveqi 5875

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

Syntax hints:   = wceq 1542  ^◡ccnv 5676

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-cnv 5685

This theorem is referenced by:  mptcnv  6140  cnvin  6145  cnvxp  6157  xp0  6158  imainrect  6181  cnvcnv  6192  cnvrescnv  6195  mptpreima  6238  co01  6261  coi2  6263  funcnvpr  6611  funcnvtp  6612  fcoi1  6766  f1oprswap  6878  f1ocnvd  7657  f1iun  7930  cnvoprab  8046  fparlem3  8100  fparlem4  8101  tz7.48-2  8442  mapsncnv  8887  sbthlem8  9090  1sdomOLD  9249  cnvepnep  9603  infxpenc2  10017  compsscnv  10366  zorn2lem4  10494  funcnvs1  14863  fsumcom2  15720  fprodcom2  15928  fthoppc  17874  oduval  18241  oduleval  18242  pjdm  21262  qtopres  23202  xkocnv  23318  ustneism  23728  mbfres  25161  dflog2  26069  dfrelog  26074  dvlog  26159  efopnlem2  26165  axcontlem2  28254  2trld  29223  0pth  29409  1pthdlem1  29419  1trld  29426  3trld  29456  ex-cnv  29721  cnvadj  31176  cnvprop  31949  gtiso  31953  padct  31975  cnvoprabOLD  31976  f1od2  31977  ordtcnvNEW  32931  ordtrest2NEW  32934  mbfmcst  33289  0rrv  33481  ballotlemrinv  33563  mthmpps  34604  pprodcnveq  34886  br1cnvres  37185  brcnvrabga  37259  dfxrn2  37294  xrninxp  37310  prjspeclsp  41402  cytpval  41999  resnonrel  42391  cononrel1  42393  cononrel2  42394  cnvtrrel  42469  clsneicnv  42904  neicvgnvo  42914