Theorem cnveqd 5819

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ss 3902  df-br 5075  df-opab 5137  df-cnv 5628

This theorem is referenced by:  opswap  6182  cores2  6213  fimacnvinrn  7012  nvocnv  7225  2ndval2  7949  2nd1st  7980  cnvf1olem  8049  fparlem3  8053  fparlem4  8054  brtpos2  8171  dftpos4  8184  tpostpos  8185  tposf12  8190  xpcomco  8994  infeq123d  9384  cantnffval2  9605  cnfcomlem  9609  fseqenlem2  9936  dfac12lem1  10055  dfac12r  10058  fpwwe2cbv  10542  fpwwe2lem2  10544  fpwwe2lem5  10547  fpwwe2lem8  10550  fpwwecbv  10556  fpwwelem  10557  funcnvs2  14864  funcnvs3  14865  funcnvs4  14866  relexpcnv  14986  fsumcnv  15724  fprodcnv  15937  bitsf1ocnv  16402  vdwpc  16940  imasval  17464  xpsval  17523  monfval  17688  ismon  17689  monpropd  17693  isepi  17696  invffval  17714  invfval  17715  dfiso2  17728  isofn  17731  oppcinv  17736  isfth  17872  catcisolem  18066  oduval  18243  oduleval  18244  gsumvalx  18633  grpinvcnv  18971  grplactcnv  19008  eqglact  19143  gsumcom2  19939  isunit  20342  issrng  20810  znval  21504  znle2  21522  evpmss  21555  psgnevpmb  21556  ptbasfi  23534  ptval2  23554  ptrescn  23592  xkoptsub  23607  qtopval  23648  txswaphmeolem  23757  ptcmpg  24010  tgplacthmeo  24056  trust  24182  prdsxmslem2  24482  metuval  24502  nghmfval  24675  isnghm  24676  pi1xfrcnv  25012  ismbf1  25579  ismbf  25583  mbfconst  25588  mbfres2  25600  cncombf  25613  deg1val  26049  fta1glem2  26122  fta1g  26123  fta1b  26125  dgrval  26181  dgrlem  26182  coe11  26206  fta1lem  26261  vieta1lem2  26265  ispth  29777  dfpth2  29785  uhgrwkspthlem2  29810  usgr2wlkspthlem1  29813  usgr2wlkspthlem2  29814  pthdlem1  29822  2spthd  29997  3spthd  30234  f1o3d  32687  xppreima2  32712  ofpreima  32726  fcnvgreu  32733  mptiffisupp  32754  fpwrelmapffslem  32793  indf1ofs  32914  gsumhashmul  33116  tocycfv  33158  tocycf  33166  cycpm2tr  33168  cycpmconjvlem  33190  evpmval  33194  altgnsg  33198  ply1dg3rt0irred  33632  vieta  33712  irngval  33817  ordtrest2NEW  34055  qqhval  34104  esum2dlem  34224  mbfmcst  34391  omssubadd  34432  sitgfval  34473  eulerpartlemgf  34511  orvcval  34590  pthhashvtx  35298  cvmliftmolem1  35451  cvmliftlem5  35459  cvmliftlem15  35468  cvmlift2lem9a  35473  cvmlift2lem9  35481  ismfs  35719  mthmval  35745  wsuceq123  35982  bj-iminvval2  37496  cnambfre  37977  itg2addnclem2  37981  ftc1anclem1  38002  ftc1anclem6  38007  dfsymrels2  38934  dfsymrel2  38942  cdlemg1finvtrlemN  41009  tendoicbv  41227  tendoi  41228  tendoi2  41229  tendoicl  41230  docaffvalN  41555  docafvalN  41556  dihmeetlem1N  41724  dihglblem5apreN  41725  diophrw  43179  rmxfval  43320  rmyfval  43321  aomclem8  43477  cnvtrclfv  44139  frege131d  44179  dssmapnvod  44435  smfpimioo  47203  smfpimcc  47224  smfsuplem2  47228  upgrimpths  48373  dftpos5  49337  tposideq  49351  invfn  49493  invpropdlem  49501  imaidfu  49573  idfth  49621  idsubc  49623  swapf1a  49732  swapf2a  49734  swapf1  49735  swapf2  49737