Theorem cnveqi 5885

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

Syntax hints:   = wceq 1540  ^◡ccnv 5684

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-cnv 5693

This theorem is referenced by:  mptcnv  6159  cnvin  6164  cnvxp  6177  xp0  6178  imainrect  6201  cnvcnv  6212  cnvrescnv  6215  mptpreima  6258  co01  6281  coi2  6283  funcnvpr  6628  funcnvtp  6629  fcoi1  6782  f1oprswap  6892  f1ocnvd  7684  resf1extb  7956  f1iun  7968  mptcnfimad  8011  cnvoprab  8085  fparlem3  8139  fparlem4  8140  tz7.48-2  8482  mapsncnv  8933  sbthlem8  9130  1sdomOLD  9285  cnvepnep  9648  infxpenc2  10062  compsscnv  10411  zorn2lem4  10539  funcnvs1  14951  fsumcom2  15810  fprodcom2  16020  fthoppc  17970  oduval  18333  oduleval  18334  pjdm  21727  qtopres  23706  xkocnv  23822  ustneism  24232  mbfres  25679  dflog2  26602  dfrelog  26607  dvlog  26693  efopnlem2  26699  axcontlem2  28980  2trld  29958  0pth  30144  1pthdlem1  30154  1trld  30161  3trld  30191  ex-cnv  30456  cnvadj  31911  cnvprop  32705  gtiso  32710  padct  32731  f1od2  32732  elrgspnsubrunlem2  33252  ordtcnvNEW  33919  ordtrest2NEW  33922  mbfmcst  34261  0rrv  34453  ballotlemrinv  34536  mthmpps  35587  pprodcnveq  35884  br1cnvres  38270  brcnvrabga  38343  dfxrn2  38377  xrninxp  38393  prjspeclsp  42622  cytpval  43214  resnonrel  43605  cononrel1  43607  cononrel2  43608  cnvtrrel  43683  clsneicnv  44118  neicvgnvo  44128  tposrescnv  48779