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 5654

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5107  df-opab 5171  df-cnv 5663

This theorem is used by:  mptcnv  6143  cnvin  6146  cnvxpOLD  6159  xp0OLD  6160  imainrect  6184  cnvcnv  6195  cnvrescnv  6199  mptpreima  6251  co01  6277  coi2  6279  funcnvpr  6621  funcnvtp  6622  fcoi1  6775  f1oprswap  6890  f1ocnvd  7693  resf1extb  7967  f1iun  7977  mptcnfimad  8019  cnvoprab  8093  f1od2  8132  fparlem3  8149  fparlem4  8150  tz7.48-2  8477  mapsncnv  8946  sbthlem8  9138  cnvepnep  9633  infxpenc2  10125  compsscnv  10473  zorn2lem4  10601  funcnvs1  15089  fsumcom2  15966  fprodcom2  16177  fthoppc  18126  oduval  18488  oduleval  18489  pjdm  22040  qtopres  24044  xkocnv  24160  ustneism  24570  mbfres  25992  dflog2  26915  dfrelog  26920  dvlog  27006  efopnlem2  27012  axcontlem2  29570  2trld  30554  0pth  30743  1pthdlem1  30753  1trld  30760  3trld  30800  ex-cnv  31065  cnvadj  32521  cnvprop  33357  gtiso  33362  padct  33378  elrgspnsubrunlem2  33876  ordtcnvNEW  34619  ordtrest2NEW  34622  mbfmcst  34958  0rrv  35150  ballotlemrinv  35233  mthmpps  36513  pprodcnveq  36822  vxp  39386  br1cnvres  39397  brcnvrabga  39465  dfxrn2  39508  xrninxp  39538  dfpre4  39603  prjspeclsp  43831  cytpval  44394  resnonrel  44782  cononrel1  44784  cononrel2  44785  cnvtrrel  44860  clsneicnv  45295  neicvgnvo  45305  upgrimpthslem1  49208  tposrescnv  50195