Theorem cnveqi 5817

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

Syntax hints:   = wceq 1540  ^◡ccnv 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3920  df-br 5093  df-opab 5155  df-cnv 5627

This theorem is referenced by:  mptcnv  6088  cnvin  6093  cnvxp  6106  xp0  6107  imainrect  6130  cnvcnv  6141  cnvrescnv  6144  mptpreima  6187  co01  6210  coi2  6212  funcnvpr  6544  funcnvtp  6545  fcoi1  6698  f1oprswap  6808  f1ocnvd  7600  resf1extb  7867  f1iun  7879  mptcnfimad  7921  cnvoprab  7995  fparlem3  8047  fparlem4  8048  tz7.48-2  8364  mapsncnv  8820  sbthlem8  9011  cnvepnep  9504  infxpenc2  9916  compsscnv  10265  zorn2lem4  10393  funcnvs1  14819  fsumcom2  15681  fprodcom2  15891  fthoppc  17832  oduval  18194  oduleval  18195  pjdm  21614  qtopres  23583  xkocnv  23699  ustneism  24109  mbfres  25543  dflog2  26467  dfrelog  26472  dvlog  26558  efopnlem2  26564  axcontlem2  28914  2trld  29887  0pth  30073  1pthdlem1  30083  1trld  30090  3trld  30120  ex-cnv  30385  cnvadj  31840  cnvprop  32646  gtiso  32651  padct  32670  f1od2  32671  elrgspnsubrunlem2  33197  ordtcnvNEW  33903  ordtrest2NEW  33906  mbfmcst  34243  0rrv  34435  ballotlemrinv  34518  mthmpps  35575  pprodcnveq  35877  br1cnvres  38264  brcnvrabga  38330  dfxrn2  38364  xrninxp  38384  prjspeclsp  42605  cytpval  43195  resnonrel  43585  cononrel1  43587  cononrel2  43588  cnvtrrel  43663  clsneicnv  44098  neicvgnvo  44108  upgrimpthslem1  47911  tposrescnv  48883