Theorem cnveqi 5852

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-br 5104  df-opab 5168  df-cnv 5659

This theorem is used by:  mptcnv  6132  cnvin  6135  cnvxpOLD  6148  xp0OLD  6149  imainrect  6173  cnvcnv  6184  cnvrescnv  6188  mptpreima  6239  co01  6263  coi2  6265  funcnvpr  6602  funcnvtp  6603  fcoi1  6756  f1oprswap  6870  f1ocnvd  7672  resf1extb  7946  f1iun  7956  mptcnfimad  7998  cnvoprab  8071  fparlem3  8125  fparlem4  8126  tz7.48-2  8452  mapsncnv  8921  sbthlem8  9113  cnvepnep  9609  infxpenc2  10101  compsscnv  10449  zorn2lem4  10577  funcnvs1  15063  fsumcom2  15940  fprodcom2  16151  fthoppc  18100  oduval  18462  oduleval  18463  pjdm  22013  qtopres  24017  xkocnv  24133  ustneism  24543  mbfres  25965  dflog2  26888  dfrelog  26893  dvlog  26979  efopnlem2  26985  axcontlem2  29543  2trld  30527  0pth  30716  1pthdlem1  30726  1trld  30733  3trld  30773  ex-cnv  31038  cnvadj  32494  cnvprop  33289  gtiso  33294  padct  33310  f1od2  33311  elrgspnsubrunlem2  33809  ordtcnvNEW  34552  ordtrest2NEW  34555  mbfmcst  34891  0rrv  35083  ballotlemrinv  35166  mthmpps  36347  pprodcnveq  36645  vxp  39195  br1cnvres  39206  brcnvrabga  39274  dfxrn2  39317  xrninxp  39347  dfpre4  39412  prjspeclsp  43640  cytpval  44203  resnonrel  44591  cononrel1  44593  cononrel2  44594  cnvtrrel  44669  clsneicnv  45104  neicvgnvo  45114  upgrimpthslem1  49004  tposrescnv  49986