Theorem cnveqi 5818

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

Syntax hints:   = wceq 1542  ^◡ccnv 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ss 3902  df-br 5075  df-opab 5137  df-cnv 5628

This theorem is referenced by:  mptcnv  6091  cnvin  6097  cnvxp  6110  xp0OLD  6111  imainrect  6134  cnvcnv  6145  cnvrescnv  6148  mptpreima  6191  co01  6215  coi2  6217  funcnvpr  6549  funcnvtp  6550  fcoi1  6703  f1oprswap  6814  f1ocnvd  7607  resf1extb  7874  f1iun  7886  mptcnfimad  7928  cnvoprab  8002  fparlem3  8053  fparlem4  8054  tz7.48-2  8370  mapsncnv  8830  sbthlem8  9021  cnvepnep  9518  infxpenc2  9933  compsscnv  10282  zorn2lem4  10410  funcnvs1  14863  fsumcom2  15725  fprodcom2  15938  fthoppc  17881  oduval  18243  oduleval  18244  pjdm  21676  qtopres  23651  xkocnv  23767  ustneism  24177  mbfres  25599  dflog2  26512  dfrelog  26517  dvlog  26603  efopnlem2  26609  axcontlem2  29022  2trld  29994  0pth  30183  1pthdlem1  30193  1trld  30200  3trld  30230  ex-cnv  30495  cnvadj  31951  cnvprop  32757  gtiso  32762  padct  32779  f1od2  32780  elrgspnsubrunlem2  33297  ordtcnvNEW  34052  ordtrest2NEW  34055  mbfmcst  34391  0rrv  34583  ballotlemrinv  34666  mthmpps  35752  pprodcnveq  36051  vxp  38572  br1cnvres  38583  brcnvrabga  38651  dfxrn2  38694  xrninxp  38724  dfpre4  38789  prjspeclsp  43033  cytpval  43618  resnonrel  44007  cononrel1  44009  cononrel2  44010  cnvtrrel  44085  clsneicnv  44520  neicvgnvo  44530  upgrimpthslem1  48371  tposrescnv  49342