Theorem cnveqi 5824

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

Syntax hints:   = wceq 1542  ^◡ccnv 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3919  df-br 5100  df-opab 5162  df-cnv 5633

This theorem is referenced by:  mptcnv  6097  cnvin  6103  cnvxp  6116  xp0OLD  6117  imainrect  6140  cnvcnv  6151  cnvrescnv  6154  mptpreima  6197  co01  6221  coi2  6223  funcnvpr  6555  funcnvtp  6556  fcoi1  6709  f1oprswap  6820  f1ocnvd  7612  resf1extb  7879  f1iun  7891  mptcnfimad  7933  cnvoprab  8007  fparlem3  8059  fparlem4  8060  tz7.48-2  8376  mapsncnv  8836  sbthlem8  9027  cnvepnep  9522  infxpenc2  9937  compsscnv  10286  zorn2lem4  10414  funcnvs1  14840  fsumcom2  15702  fprodcom2  15912  fthoppc  17854  oduval  18216  oduleval  18217  pjdm  21667  qtopres  23647  xkocnv  23763  ustneism  24173  mbfres  25606  dflog2  26530  dfrelog  26535  dvlog  26621  efopnlem2  26627  axcontlem2  29043  2trld  30016  0pth  30205  1pthdlem1  30215  1trld  30222  3trld  30252  ex-cnv  30517  cnvadj  31972  cnvprop  32778  gtiso  32783  padct  32800  f1od2  32801  elrgspnsubrunlem2  33334  ordtcnvNEW  34090  ordtrest2NEW  34093  mbfmcst  34429  0rrv  34621  ballotlemrinv  34704  mthmpps  35789  pprodcnveq  36088  vxp  38477  br1cnvres  38488  brcnvrabga  38556  dfxrn2  38599  xrninxp  38629  dfpre4  38694  prjspeclsp  42933  cytpval  43522  resnonrel  43911  cononrel1  43913  cononrel2  43914  cnvtrrel  43989  clsneicnv  44424  neicvgnvo  44434  upgrimpthslem1  48230  tposrescnv  49201