Theorem cnveqd 5829

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

Syntax hints:   → wi 4   = 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:  opswap  6190  cores2  6220  fimacnvinrn  7025  nvocnv  7238  2ndval2  7965  2nd1st  7996  cnvf1olem  8066  fparlem3  8070  fparlem4  8071  brtpos2  8188  dftpos4  8201  tpostpos  8202  tposf12  8207  xpcomco  9008  infeq123d  9409  cantnffval2  9624  cnfcomlem  9628  fseqenlem2  9954  dfac12lem1  10073  dfac12r  10076  fpwwe2cbv  10559  fpwwe2lem2  10561  fpwwe2lem5  10564  fpwwe2lem8  10567  fpwwecbv  10573  fpwwelem  10574  funcnvs2  14855  funcnvs3  14856  funcnvs4  14857  relexpcnv  14977  fsumcnv  15715  fprodcnv  15925  bitsf1ocnv  16390  vdwpc  16927  imasval  17450  xpsval  17509  monfval  17674  ismon  17675  monpropd  17679  isepi  17682  invffval  17700  invfval  17701  dfiso2  17714  isofn  17717  oppcinv  17722  isfth  17858  catcisolem  18052  oduval  18229  oduleval  18230  gsumvalx  18585  grpinvcnv  18920  grplactcnv  18957  eqglact  19093  gsumcom2  19889  isunit  20293  issrng  20764  znval  21477  znle2  21495  evpmss  21528  psgnevpmb  21529  ptbasfi  23501  ptval2  23521  ptrescn  23559  xkoptsub  23574  qtopval  23615  txswaphmeolem  23724  ptcmpg  23977  tgplacthmeo  24023  trust  24150  prdsxmslem2  24450  metuval  24470  nghmfval  24643  isnghm  24644  pi1xfrcnv  24990  ismbf1  25558  ismbf  25562  mbfconst  25567  mbfres2  25579  cncombf  25592  deg1val  26034  fta1glem2  26107  fta1g  26108  fta1b  26110  dgrval  26166  dgrlem  26167  coe11  26191  fta1lem  26248  vieta1lem2  26252  ispth  29701  dfpth2  29709  uhgrwkspthlem2  29734  usgr2wlkspthlem1  29737  usgr2wlkspthlem2  29738  pthdlem1  29746  2spthd  29921  3spthd  30155  f1o3d  32601  xppreima2  32625  ofpreima  32639  fcnvgreu  32647  mptiffisupp  32666  fpwrelmapffslem  32705  indf1ofs  32839  gsumhashmul  33044  tocycfv  33081  tocycf  33089  cycpm2tr  33091  cycpmconjvlem  33113  evpmval  33117  altgnsg  33121  ply1dg3rt0irred  33544  irngval  33673  ordtrest2NEW  33906  qqhval  33955  esum2dlem  34075  mbfmcst  34243  omssubadd  34284  sitgfval  34325  eulerpartlemgf  34363  orvcval  34442  pthhashvtx  35108  cvmliftmolem1  35261  cvmliftlem5  35269  cvmliftlem15  35278  cvmlift2lem9a  35283  cvmlift2lem9  35291  ismfs  35529  mthmval  35555  wsuceq123  35795  bj-iminvval2  37175  cnambfre  37655  itg2addnclem2  37659  ftc1anclem1  37680  ftc1anclem6  37685  dfsymrels2  38529  dfsymrel2  38533  cdlemg1finvtrlemN  40562  tendoicbv  40780  tendoi  40781  tendoi2  40782  tendoicl  40783  docaffvalN  41108  docafvalN  41109  dihmeetlem1N  41277  dihglblem5apreN  41278  diophrw  42740  rmxfval  42885  rmyfval  42886  aomclem8  43043  cnvtrclfv  43706  frege131d  43746  dssmapnvod  44002  smfpimioo  46778  smfpimcc  46799  smfsuplem2  46803  upgrimpths  47902  dftpos5  48855  tposideq  48869  invfn  49012  invpropdlem  49020  imaidfu  49092  idfth  49140  idsubc  49142  swapf1a  49251  swapf2a  49253  swapf1  49254  swapf2  49256