Theorem cnveqi 5848

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

This proof depends on syntax axioms:   = wceq 1570  ^◡ccnv 5646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3915  df-br 5103  df-opab 5167  df-cnv 5655

This theorem is used by:  mptcnv  6126  cnvin  6129  cnvxpOLD  6143  xp0OLD  6144  imainrect  6168  cnvcnv  6179  cnvrescnv  6183  mptpreima  6228  co01  6252  coi2  6254  funcnvpr  6590  funcnvtp  6591  fcoi1  6744  f1oprswap  6858  f1ocnvd  7660  resf1extb  7929  f1iun  7939  mptcnfimad  7981  cnvoprab  8054  fparlem3  8108  fparlem4  8109  tz7.48-2  8430  mapsncnv  8899  sbthlem8  9091  cnvepnep  9587  infxpenc2  10072  compsscnv  10420  zorn2lem4  10548  funcnvs1  15030  fsumcom2  15907  fprodcom2  16118  fthoppc  18061  oduval  18423  oduleval  18424  pjdm  21974  qtopres  23978  xkocnv  24094  ustneism  24504  mbfres  25926  dflog2  26851  dfrelog  26856  dvlog  26942  efopnlem2  26948  axcontlem2  29476  2trld  30460  0pth  30649  1pthdlem1  30659  1trld  30666  3trld  30706  ex-cnv  30971  cnvadj  32427  cnvprop  33222  gtiso  33227  padct  33243  f1od2  33244  elrgspnsubrunlem2  33742  ordtcnvNEW  34485  ordtrest2NEW  34488  mbfmcst  34825  0rrv  35017  ballotlemrinv  35100  mthmpps  36268  pprodcnveq  36567  vxp  39115  br1cnvres  39126  brcnvrabga  39194  dfxrn2  39237  xrninxp  39267  dfpre4  39332  prjspeclsp  43562  cytpval  44147  resnonrel  44536  cononrel1  44538  cononrel2  44539  cnvtrrel  44614  clsneicnv  45049  neicvgnvo  45059  upgrimpthslem1  48927  tposrescnv  49909