Theorem cnveqd 5888

Description: Equality deduction for converse relation. (Contributed by NM, 6-Dec-2013.)

Hypothesis

Ref	Expression
cnveqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
cnveqd	⊢ (𝜑 → ◡𝐴 = ◡𝐵)

Proof of Theorem cnveqd

Step	Hyp	Ref	Expression
1		cnveqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		cnveq 5886	. 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   = wceq 1536  ^◡ccnv 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-br 5148  df-opab 5210  df-cnv 5696

This theorem is referenced by:  opswap  6250  cores2  6280  fimacnvinrn  7090  nvocnv  7300  2ndval2  8030  2nd1st  8061  cnvf1olem  8133  fparlem3  8137  fparlem4  8138  brtpos2  8255  dftpos4  8268  tpostpos  8269  tposf12  8274  xpcomco  9100  infeq123d  9518  cantnffval2  9732  cnfcomlem  9736  fseqenlem2  10062  dfac12lem1  10181  dfac12r  10184  fpwwe2cbv  10667  fpwwe2lem2  10669  fpwwe2lem5  10672  fpwwe2lem8  10675  fpwwecbv  10681  fpwwelem  10682  funcnvs2  14948  funcnvs3  14949  funcnvs4  14950  relexpcnv  15070  fsumcnv  15805  fprodcnv  16015  bitsf1ocnv  16477  vdwpc  17013  imasval  17557  xpsval  17616  monfval  17779  ismon  17780  monpropd  17784  isepi  17787  invffval  17805  invfval  17806  dfiso2  17819  isofn  17822  oppcinv  17827  isfth  17967  catcisolem  18163  oduval  18344  oduleval  18345  gsumvalx  18701  grpinvcnv  19036  grplactcnv  19073  eqglact  19209  gsumcom2  20007  isunit  20389  issrng  20861  znval  21567  znle2  21589  evpmss  21621  psgnevpmb  21622  ptbasfi  23604  ptval2  23624  ptrescn  23662  xkoptsub  23677  qtopval  23718  txswaphmeolem  23827  ptcmpg  24080  tgplacthmeo  24126  trust  24253  prdsxmslem2  24557  metuval  24577  nghmfval  24758  isnghm  24759  pi1xfrcnv  25103  ismbf1  25672  ismbf  25676  mbfconst  25681  mbfres2  25693  cncombf  25706  deg1val  26149  fta1glem2  26222  fta1g  26223  fta1b  26225  dgrval  26281  dgrlem  26282  coe11  26306  fta1lem  26363  vieta1lem2  26367  ispth  29755  uhgrwkspthlem2  29786  usgr2wlkspthlem1  29789  usgr2wlkspthlem2  29790  pthdlem1  29798  2spthd  29970  3spthd  30204  f1o3d  32643  xppreima2  32667  ofpreima  32681  fcnvgreu  32689  mptiffisupp  32707  fpwrelmapffslem  32749  gsumhashmul  33046  tocycfv  33111  tocycf  33119  cycpm2tr  33121  cycpmconjvlem  33143  evpmval  33147  altgnsg  33151  ply1dg3rt0irred  33586  irngval  33699  ordtrest2NEW  33883  qqhval  33934  indf1ofs  34006  esum2dlem  34072  mbfmcst  34240  omssubadd  34281  sitgfval  34322  eulerpartlemgf  34360  orvcval  34438  pthhashvtx  35111  cvmliftmolem1  35265  cvmliftlem5  35273  cvmliftlem15  35282  cvmlift2lem9a  35287  cvmlift2lem9  35295  ismfs  35533  mthmval  35559  wsuceq123  35795  bj-iminvval2  37176  cnambfre  37654  itg2addnclem2  37658  ftc1anclem1  37679  ftc1anclem6  37684  dfsymrels2  38526  dfsymrel2  38530  cdlemg1finvtrlemN  40557  tendoicbv  40775  tendoi  40776  tendoi2  40777  tendoicl  40778  docaffvalN  41103  docafvalN  41104  dihmeetlem1N  41272  dihglblem5apreN  41273  diophrw  42746  rmxfval  42891  rmyfval  42892  aomclem8  43049  cnvtrclfv  43713  frege131d  43753  dssmapnvod  44009  smfpimioo  46742  smfpimcc  46763  smfsuplem2  46767