Theorem cnveqd 5828

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

Syntax hints:   → wi 4   = wceq 1542  ^◡ccnv 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-br 5087  df-opab 5149  df-cnv 5636

This theorem is referenced by:  opswap  6191  cores2  6222  fimacnvinrn  7021  nvocnv  7233  2ndval2  7957  2nd1st  7988  cnvf1olem  8057  fparlem3  8061  fparlem4  8062  brtpos2  8179  dftpos4  8192  tpostpos  8193  tposf12  8198  xpcomco  9002  infeq123d  9392  cantnffval2  9613  cnfcomlem  9617  fseqenlem2  9944  dfac12lem1  10063  dfac12r  10066  fpwwe2cbv  10550  fpwwe2lem2  10552  fpwwe2lem5  10555  fpwwe2lem8  10558  fpwwecbv  10564  fpwwelem  10565  funcnvs2  14872  funcnvs3  14873  funcnvs4  14874  relexpcnv  14994  fsumcnv  15732  fprodcnv  15945  bitsf1ocnv  16410  vdwpc  16948  imasval  17472  xpsval  17531  monfval  17696  ismon  17697  monpropd  17701  isepi  17704  invffval  17722  invfval  17723  dfiso2  17736  isofn  17739  oppcinv  17744  isfth  17880  catcisolem  18074  oduval  18251  oduleval  18252  gsumvalx  18641  grpinvcnv  18979  grplactcnv  19016  eqglact  19151  gsumcom2  19947  isunit  20350  issrng  20818  znval  21531  znle2  21549  evpmss  21582  psgnevpmb  21583  ptbasfi  23562  ptval2  23582  ptrescn  23620  xkoptsub  23635  qtopval  23676  txswaphmeolem  23785  ptcmpg  24038  tgplacthmeo  24084  trust  24210  prdsxmslem2  24510  metuval  24530  nghmfval  24703  isnghm  24704  pi1xfrcnv  25040  ismbf1  25607  ismbf  25611  mbfconst  25616  mbfres2  25628  cncombf  25641  deg1val  26077  fta1glem2  26150  fta1g  26151  fta1b  26153  dgrval  26209  dgrlem  26210  coe11  26234  fta1lem  26290  vieta1lem2  26294  ispth  29810  dfpth2  29818  uhgrwkspthlem2  29843  usgr2wlkspthlem1  29846  usgr2wlkspthlem2  29847  pthdlem1  29855  2spthd  30030  3spthd  30267  f1o3d  32720  xppreima2  32745  ofpreima  32759  fcnvgreu  32766  mptiffisupp  32787  fpwrelmapffslem  32826  indf1ofs  32947  gsumhashmul  33149  tocycfv  33191  tocycf  33199  cycpm2tr  33201  cycpmconjvlem  33223  evpmval  33227  altgnsg  33231  ply1dg3rt0irred  33665  vieta  33745  irngval  33851  ordtrest2NEW  34089  qqhval  34138  esum2dlem  34258  mbfmcst  34425  omssubadd  34466  sitgfval  34507  eulerpartlemgf  34545  orvcval  34624  pthhashvtx  35332  cvmliftmolem1  35485  cvmliftlem5  35493  cvmliftlem15  35502  cvmlift2lem9a  35507  cvmlift2lem9  35515  ismfs  35753  mthmval  35779  wsuceq123  36016  bj-iminvval2  37530  cnambfre  38011  itg2addnclem2  38015  ftc1anclem1  38036  ftc1anclem6  38041  dfsymrels2  38968  dfsymrel2  38976  cdlemg1finvtrlemN  41043  tendoicbv  41261  tendoi  41262  tendoi2  41263  tendoicl  41264  docaffvalN  41589  docafvalN  41590  dihmeetlem1N  41758  dihglblem5apreN  41759  diophrw  43213  rmxfval  43358  rmyfval  43359  aomclem8  43515  cnvtrclfv  44177  frege131d  44217  dssmapnvod  44473  smfpimioo  47241  smfpimcc  47262  smfsuplem2  47266  upgrimpths  48405  dftpos5  49369  tposideq  49383  invfn  49525  invpropdlem  49533  imaidfu  49605  idfth  49653  idsubc  49655  swapf1a  49764  swapf2a  49766  swapf1  49767  swapf2  49769