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  28223  2trld  29192  0pth  29378  1pthdlem1  29388  1trld  29395  3trld  29425  ex-cnv  29690  cnvadj  31145  cnvprop  31918  gtiso  31922  padct  31944  cnvoprabOLD  31945  f1od2  31946  ordtcnvNEW  32900  ordtrest2NEW  32903  mbfmcst  33258  0rrv  33450  ballotlemrinv  33532  mthmpps  34573  pprodcnveq  34855  br1cnvres  37137  brcnvrabga  37211  dfxrn2  37246  xrninxp  37262  prjspeclsp  41354  cytpval  41951  resnonrel  42343  cononrel1  42345  cononrel2  42346  cnvtrrel  42421  clsneicnv  42856  neicvgnvo  42866