Theorem cnveqi 5851

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

This proof depends on syntax axioms:   = wceq 1569  ^◡ccnv 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-br 5103  df-opab 5167  df-cnv 5658

This theorem is used by:  mptcnv  6131  cnvin  6134  cnvxpOLD  6147  xp0OLD  6148  imainrect  6172  cnvcnv  6183  cnvrescnv  6187  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  39196  br1cnvres  39207  brcnvrabga  39275  dfxrn2  39318  xrninxp  39348  dfpre4  39413  prjspeclsp  43641  cytpval  44204  resnonrel  44592  cononrel1  44594  cononrel2  44595  cnvtrrel  44670  clsneicnv  45105  neicvgnvo  45115  upgrimpthslem1  49005  tposrescnv  49987