Theorem cnveqi 5829

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

Syntax hints:   = wceq 1540  ^◡ccnv 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-br 5103  df-opab 5165  df-cnv 5639

This theorem is referenced by:  mptcnv  6101  cnvin  6106  cnvxp  6119  xp0  6120  imainrect  6143  cnvcnv  6154  cnvrescnv  6157  mptpreima  6200  co01  6223  coi2  6225  funcnvpr  6563  funcnvtp  6564  fcoi1  6717  f1oprswap  6827  f1ocnvd  7621  resf1extb  7891  f1iun  7903  mptcnfimad  7945  cnvoprab  8019  fparlem3  8071  fparlem4  8072  tz7.48-2  8388  mapsncnv  8844  sbthlem8  9036  1sdomOLD  9173  cnvepnep  9540  infxpenc2  9954  compsscnv  10303  zorn2lem4  10431  funcnvs1  14856  fsumcom2  15718  fprodcom2  15928  fthoppc  17869  oduval  18231  oduleval  18232  pjdm  21651  qtopres  23620  xkocnv  23736  ustneism  24146  mbfres  25580  dflog2  26504  dfrelog  26509  dvlog  26595  efopnlem2  26601  axcontlem2  28947  2trld  29920  0pth  30106  1pthdlem1  30116  1trld  30123  3trld  30153  ex-cnv  30418  cnvadj  31873  cnvprop  32671  gtiso  32676  padct  32695  f1od2  32696  elrgspnsubrunlem2  33217  ordtcnvNEW  33905  ordtrest2NEW  33908  mbfmcst  34245  0rrv  34437  ballotlemrinv  34520  mthmpps  35564  pprodcnveq  35866  br1cnvres  38253  brcnvrabga  38319  dfxrn2  38353  xrninxp  38373  prjspeclsp  42595  cytpval  43186  resnonrel  43576  cononrel1  43578  cononrel2  43579  cnvtrrel  43654  clsneicnv  44089  neicvgnvo  44099  upgrimpthslem1  47902  tposrescnv  48862