Theorem cnveqd 5839

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

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

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 3931  df-br 5108  df-opab 5170  df-cnv 5646

This theorem is referenced by:  opswap  6202  cores2  6232  fimacnvinrn  7043  nvocnv  7256  2ndval2  7986  2nd1st  8017  cnvf1olem  8089  fparlem3  8093  fparlem4  8094  brtpos2  8211  dftpos4  8224  tpostpos  8225  tposf12  8230  xpcomco  9031  infeq123d  9433  cantnffval2  9648  cnfcomlem  9652  fseqenlem2  9978  dfac12lem1  10097  dfac12r  10100  fpwwe2cbv  10583  fpwwe2lem2  10585  fpwwe2lem5  10588  fpwwe2lem8  10591  fpwwecbv  10597  fpwwelem  10598  funcnvs2  14879  funcnvs3  14880  funcnvs4  14881  relexpcnv  15001  fsumcnv  15739  fprodcnv  15949  bitsf1ocnv  16414  vdwpc  16951  imasval  17474  xpsval  17533  monfval  17694  ismon  17695  monpropd  17699  isepi  17702  invffval  17720  invfval  17721  dfiso2  17734  isofn  17737  oppcinv  17742  isfth  17878  catcisolem  18072  oduval  18249  oduleval  18250  gsumvalx  18603  grpinvcnv  18938  grplactcnv  18975  eqglact  19111  gsumcom2  19905  isunit  20282  issrng  20753  znval  21445  znle2  21463  evpmss  21495  psgnevpmb  21496  ptbasfi  23468  ptval2  23488  ptrescn  23526  xkoptsub  23541  qtopval  23582  txswaphmeolem  23691  ptcmpg  23944  tgplacthmeo  23990  trust  24117  prdsxmslem2  24417  metuval  24437  nghmfval  24610  isnghm  24611  pi1xfrcnv  24957  ismbf1  25525  ismbf  25529  mbfconst  25534  mbfres2  25546  cncombf  25559  deg1val  26001  fta1glem2  26074  fta1g  26075  fta1b  26077  dgrval  26133  dgrlem  26134  coe11  26158  fta1lem  26215  vieta1lem2  26219  ispth  29651  dfpth2  29659  uhgrwkspthlem2  29684  usgr2wlkspthlem1  29687  usgr2wlkspthlem2  29688  pthdlem1  29696  2spthd  29871  3spthd  30105  f1o3d  32551  xppreima2  32575  ofpreima  32589  fcnvgreu  32597  mptiffisupp  32616  fpwrelmapffslem  32655  indf1ofs  32789  gsumhashmul  33001  tocycfv  33066  tocycf  33074  cycpm2tr  33076  cycpmconjvlem  33098  evpmval  33102  altgnsg  33106  ply1dg3rt0irred  33551  irngval  33680  ordtrest2NEW  33913  qqhval  33962  esum2dlem  34082  mbfmcst  34250  omssubadd  34291  sitgfval  34332  eulerpartlemgf  34370  orvcval  34449  pthhashvtx  35115  cvmliftmolem1  35268  cvmliftlem5  35276  cvmliftlem15  35285  cvmlift2lem9a  35290  cvmlift2lem9  35298  ismfs  35536  mthmval  35562  wsuceq123  35802  bj-iminvval2  37182  cnambfre  37662  itg2addnclem2  37666  ftc1anclem1  37687  ftc1anclem6  37692  dfsymrels2  38536  dfsymrel2  38540  cdlemg1finvtrlemN  40569  tendoicbv  40787  tendoi  40788  tendoi2  40789  tendoicl  40790  docaffvalN  41115  docafvalN  41116  dihmeetlem1N  41284  dihglblem5apreN  41285  diophrw  42747  rmxfval  42892  rmyfval  42893  aomclem8  43050  cnvtrclfv  43713  frege131d  43753  dssmapnvod  44009  smfpimioo  46785  smfpimcc  46806  smfsuplem2  46810  upgrimpths  47909  dftpos5  48862  tposideq  48876  invfn  49019  invpropdlem  49027  imaidfu  49099  idfth  49147  idsubc  49149  swapf1a  49258  swapf2a  49260  swapf1  49261  swapf2  49263