Theorem cnveqi 5899

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

Syntax hints:   = wceq 1537  ^◡ccnv 5699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-cnv 5708

This theorem is referenced by:  mptcnv  6171  cnvin  6176  cnvxp  6188  xp0  6189  imainrect  6212  cnvcnv  6223  cnvrescnv  6226  mptpreima  6269  co01  6292  coi2  6294  funcnvpr  6640  funcnvtp  6641  fcoi1  6795  f1oprswap  6906  f1ocnvd  7701  f1iun  7984  mptcnfimad  8027  cnvoprab  8101  fparlem3  8155  fparlem4  8156  tz7.48-2  8498  mapsncnv  8951  sbthlem8  9156  1sdomOLD  9312  cnvepnep  9677  infxpenc2  10091  compsscnv  10440  zorn2lem4  10568  funcnvs1  14961  fsumcom2  15822  fprodcom2  16032  fthoppc  17990  oduval  18358  oduleval  18359  pjdm  21750  qtopres  23727  xkocnv  23843  ustneism  24253  mbfres  25698  dflog2  26620  dfrelog  26625  dvlog  26711  efopnlem2  26717  axcontlem2  28998  2trld  29971  0pth  30157  1pthdlem1  30167  1trld  30174  3trld  30204  ex-cnv  30469  cnvadj  31924  cnvprop  32708  gtiso  32712  padct  32733  cnvoprabOLD  32734  f1od2  32735  ordtcnvNEW  33866  ordtrest2NEW  33869  mbfmcst  34224  0rrv  34416  ballotlemrinv  34498  mthmpps  35550  pprodcnveq  35847  br1cnvres  38225  brcnvrabga  38298  dfxrn2  38332  xrninxp  38348  prjspeclsp  42567  cytpval  43163  resnonrel  43554  cononrel1  43556  cononrel2  43557  cnvtrrel  43632  clsneicnv  44067  neicvgnvo  44077