Theorem cnveqd 5787

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

Syntax hints:   → wi 4   = wceq 1539  ^◡ccnv 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-br 5076  df-opab 5138  df-cnv 5598

This theorem is referenced by:  opswap  6137  cores2  6167  fimacnvinrn  6958  nvocnv  7162  2ndval2  7858  2nd1st  7888  cnvf1olem  7959  fparlem3  7963  fparlem4  7964  brtpos2  8057  dftpos4  8070  tpostpos  8071  tposf12  8076  xpcomco  8858  infeq123d  9249  cantnffval2  9462  cnfcomlem  9466  fseqenlem2  9790  dfac12lem1  9908  dfac12r  9911  fpwwe2cbv  10395  fpwwe2lem2  10397  fpwwe2lem5  10400  fpwwe2lem8  10403  fpwwecbv  10409  fpwwelem  10410  funcnvs2  14635  funcnvs3  14636  funcnvs4  14637  relexpcnv  14755  fsumcnv  15494  fprodcnv  15702  bitsf1ocnv  16160  vdwpc  16690  imasval  17231  xpsval  17290  monfval  17453  ismon  17454  monpropd  17458  isepi  17461  invffval  17479  invfval  17480  dfiso2  17493  isofn  17496  oppcinv  17501  isfth  17639  catcisolem  17834  oduval  18015  oduleval  18016  gsumvalx  18369  grpinvcnv  18652  grplactcnv  18687  eqglact  18816  gsumcom2  19585  isunit  19908  issrng  20119  znval  20748  znle2  20770  evpmss  20800  psgnevpmb  20801  ptbasfi  22741  ptval2  22761  ptrescn  22799  xkoptsub  22814  qtopval  22855  txswaphmeolem  22964  ptcmpg  23217  tgplacthmeo  23263  trust  23390  prdsxmslem2  23694  metuval  23714  nghmfval  23895  isnghm  23896  pi1xfrcnv  24229  ismbf1  24797  ismbf  24801  mbfconst  24806  mbfres2  24818  cncombf  24831  deg1val  25270  fta1glem2  25340  fta1g  25341  fta1b  25343  dgrval  25398  dgrlem  25399  coe11  25423  fta1lem  25476  vieta1lem2  25480  ispth  28100  uhgrwkspthlem2  28131  usgr2wlkspthlem1  28134  usgr2wlkspthlem2  28135  pthdlem1  28143  2spthd  28315  3spthd  28549  f1o3d  30971  xppreima2  30997  ofpreima  31011  fcnvgreu  31019  fpwrelmapffslem  31076  gsumhashmul  31325  tocycfv  31385  tocycf  31393  cycpm2tr  31395  cycpmconjvlem  31417  evpmval  31421  altgnsg  31425  ordtrest2NEW  31882  qqhval  31933  indf1ofs  32003  esum2dlem  32069  mbfmcst  32235  omssubadd  32276  sitgfval  32317  eulerpartlemgf  32355  orvcval  32433  pthhashvtx  33098  cvmliftmolem1  33252  cvmliftlem5  33260  cvmliftlem15  33269  cvmlift2lem9a  33274  cvmlift2lem9  33282  ismfs  33520  mthmval  33546  wsuceq123  33817  bj-iminvval2  35374  cnambfre  35834  itg2addnclem2  35838  ftc1anclem1  35859  ftc1anclem6  35864  dfsymrels2  36666  dfsymrel2  36670  cdlemg1finvtrlemN  38596  tendoicbv  38814  tendoi  38815  tendoi2  38816  tendoicl  38817  docaffvalN  39142  docafvalN  39143  dihmeetlem1N  39311  dihglblem5apreN  39312  diophrw  40588  rmxfval  40733  rmyfval  40734  aomclem8  40893  cnvtrclfv  41339  frege131d  41379  dssmapnvod  41635  smfpimioo  44332  smfpimcc  44352  smfsuplem2  44356