Theorem cnveqi 5858

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3919  df-br 5108  df-opab 5172  df-cnv 5667

This theorem is used by:  mptcnv  6136  cnvin  6139  cnvxpOLD  6153  xp0OLD  6154  imainrect  6178  cnvcnv  6189  cnvrescnv  6193  mptpreima  6238  co01  6262  coi2  6264  funcnvpr  6599  funcnvtp  6600  fcoi1  6753  f1oprswap  6867  f1ocnvd  7668  resf1extb  7934  f1iun  7944  mptcnfimad  7986  cnvoprab  8060  fparlem3  8114  fparlem4  8115  tz7.48-2  8434  mapsncnv  8903  sbthlem8  9095  cnvepnep  9590  infxpenc2  10028  compsscnv  10376  zorn2lem4  10504  funcnvs1  14985  fsumcom2  15862  fprodcom2  16075  fthoppc  18018  oduval  18380  oduleval  18381  pjdm  21921  qtopres  23925  xkocnv  24041  ustneism  24451  mbfres  25873  dflog2  26795  dfrelog  26800  dvlog  26886  efopnlem2  26892  axcontlem2  29408  2trld  30392  0pth  30581  1pthdlem1  30591  1trld  30598  3trld  30638  ex-cnv  30903  cnvadj  32359  cnvprop  33155  gtiso  33160  padct  33176  f1od2  33177  elrgspnsubrunlem2  33675  ordtcnvNEW  34417  ordtrest2NEW  34420  mbfmcst  34757  0rrv  34949  ballotlemrinv  35032  mthmpps  36148  pprodcnveq  36447  vxp  38998  br1cnvres  39009  brcnvrabga  39077  dfxrn2  39120  xrninxp  39150  dfpre4  39215  prjspeclsp  43445  cytpval  44030  resnonrel  44419  cononrel1  44421  cononrel2  44422  cnvtrrel  44497  clsneicnv  44932  neicvgnvo  44942  upgrimpthslem1  48810  tposrescnv  49792