Theorem cnveqi 5745

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

Syntax hints:   = wceq 1537  ^◡ccnv 5554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3943  df-ss 3952  df-br 5067  df-opab 5129  df-cnv 5563

This theorem is referenced by:  mptcnv  5998  cnvin  6003  cnvxp  6014  xp0  6015  imainrect  6038  cnvcnv  6049  cnvrescnv  6052  mptpreima  6092  co01  6114  coi2  6116  funcnvpr  6416  funcnvtp  6417  fcoi1  6552  f1oprswap  6658  f1ocnvd  7396  f1iun  7645  cnvoprab  7758  fparlem3  7809  fparlem4  7810  tz7.48-2  8078  mapsncnv  8457  sbthlem8  8634  1sdom  8721  cnvepnep  9071  infxpenc2  9448  compsscnv  9793  zorn2lem4  9921  funcnvs1  14274  fsumcom2  15129  fprodcom2  15338  fthoppc  17193  oduval  17740  oduleval  17741  pjdm  20851  qtopres  22306  xkocnv  22422  ustneism  22832  mbfres  24245  dflog2  25144  dfrelog  25149  dvlog  25234  efopnlem2  25240  axcontlem2  26751  2trld  27717  0pth  27904  1pthdlem1  27914  1trld  27921  3trld  27951  ex-cnv  28216  cnvadj  29669  cnvprop  30432  gtiso  30436  padct  30455  cnvoprabOLD  30456  f1od2  30457  ordtcnvNEW  31163  ordtrest2NEW  31166  mbfmcst  31517  0rrv  31709  ballotlemrinv  31791  mthmpps  32829  pprodcnveq  33344  brcnvrabga  35614  dfxrn2  35643  xrninxp  35655  prjspeclsp  39282  cytpval  39829  resnonrel  39972  cononrel1  39974  cononrel2  39975  cnvtrrel  40035  clsneicnv  40475  neicvgnvo  40485