Theorem cnveqd 5842

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 5840	. 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   = wceq 1540  ^◡ccnv 5640

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-cnv 5649

This theorem is referenced by:  opswap  6205  cores2  6235  fimacnvinrn  7046  nvocnv  7259  2ndval2  7989  2nd1st  8020  cnvf1olem  8092  fparlem3  8096  fparlem4  8097  brtpos2  8214  dftpos4  8227  tpostpos  8228  tposf12  8233  xpcomco  9036  infeq123d  9440  cantnffval2  9655  cnfcomlem  9659  fseqenlem2  9985  dfac12lem1  10104  dfac12r  10107  fpwwe2cbv  10590  fpwwe2lem2  10592  fpwwe2lem5  10595  fpwwe2lem8  10598  fpwwecbv  10604  fpwwelem  10605  funcnvs2  14886  funcnvs3  14887  funcnvs4  14888  relexpcnv  15008  fsumcnv  15746  fprodcnv  15956  bitsf1ocnv  16421  vdwpc  16958  imasval  17481  xpsval  17540  monfval  17701  ismon  17702  monpropd  17706  isepi  17709  invffval  17727  invfval  17728  dfiso2  17741  isofn  17744  oppcinv  17749  isfth  17885  catcisolem  18079  oduval  18256  oduleval  18257  gsumvalx  18610  grpinvcnv  18945  grplactcnv  18982  eqglact  19118  gsumcom2  19912  isunit  20289  issrng  20760  znval  21452  znle2  21470  evpmss  21502  psgnevpmb  21503  ptbasfi  23475  ptval2  23495  ptrescn  23533  xkoptsub  23548  qtopval  23589  txswaphmeolem  23698  ptcmpg  23951  tgplacthmeo  23997  trust  24124  prdsxmslem2  24424  metuval  24444  nghmfval  24617  isnghm  24618  pi1xfrcnv  24964  ismbf1  25532  ismbf  25536  mbfconst  25541  mbfres2  25553  cncombf  25566  deg1val  26008  fta1glem2  26081  fta1g  26082  fta1b  26084  dgrval  26140  dgrlem  26141  coe11  26165  fta1lem  26222  vieta1lem2  26226  ispth  29658  dfpth2  29666  uhgrwkspthlem2  29691  usgr2wlkspthlem1  29694  usgr2wlkspthlem2  29695  pthdlem1  29703  2spthd  29878  3spthd  30112  f1o3d  32558  xppreima2  32582  ofpreima  32596  fcnvgreu  32604  mptiffisupp  32623  fpwrelmapffslem  32662  indf1ofs  32796  gsumhashmul  33008  tocycfv  33073  tocycf  33081  cycpm2tr  33083  cycpmconjvlem  33105  evpmval  33109  altgnsg  33113  ply1dg3rt0irred  33558  irngval  33687  ordtrest2NEW  33920  qqhval  33969  esum2dlem  34089  mbfmcst  34257  omssubadd  34298  sitgfval  34339  eulerpartlemgf  34377  orvcval  34456  pthhashvtx  35122  cvmliftmolem1  35275  cvmliftlem5  35283  cvmliftlem15  35292  cvmlift2lem9a  35297  cvmlift2lem9  35305  ismfs  35543  mthmval  35569  wsuceq123  35809  bj-iminvval2  37189  cnambfre  37669  itg2addnclem2  37673  ftc1anclem1  37694  ftc1anclem6  37699  dfsymrels2  38543  dfsymrel2  38547  cdlemg1finvtrlemN  40576  tendoicbv  40794  tendoi  40795  tendoi2  40796  tendoicl  40797  docaffvalN  41122  docafvalN  41123  dihmeetlem1N  41291  dihglblem5apreN  41292  diophrw  42754  rmxfval  42899  rmyfval  42900  aomclem8  43057  cnvtrclfv  43720  frege131d  43760  dssmapnvod  44016  smfpimioo  46792  smfpimcc  46813  smfsuplem2  46817  upgrimpths  47913  dftpos5  48866  tposideq  48880  invfn  49023  invpropdlem  49031  imaidfu  49103  idfth  49151  idsubc  49153  swapf1a  49262  swapf2a  49264  swapf1  49265  swapf2  49267