Theorem cnveqd 5876

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

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

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-cnv 5685

This theorem is referenced by:  opswap  6229  cores2  6259  fimacnvinrn  7074  nvocnv  7279  2ndval2  7993  2nd1st  8024  cnvf1olem  8096  fparlem3  8100  fparlem4  8101  brtpos2  8217  dftpos4  8230  tpostpos  8231  tposf12  8236  xpcomco  9062  infeq123d  9476  cantnffval2  9690  cnfcomlem  9694  fseqenlem2  10020  dfac12lem1  10138  dfac12r  10141  fpwwe2cbv  10625  fpwwe2lem2  10627  fpwwe2lem5  10630  fpwwe2lem8  10633  fpwwecbv  10639  fpwwelem  10640  funcnvs2  14864  funcnvs3  14865  funcnvs4  14866  relexpcnv  14982  fsumcnv  15719  fprodcnv  15927  bitsf1ocnv  16385  vdwpc  16913  imasval  17457  xpsval  17516  monfval  17679  ismon  17680  monpropd  17684  isepi  17687  invffval  17705  invfval  17706  dfiso2  17719  isofn  17722  oppcinv  17727  isfth  17865  catcisolem  18060  oduval  18241  oduleval  18242  gsumvalx  18595  grpinvcnv  18891  grplactcnv  18926  eqglact  19059  gsumcom2  19843  isunit  20187  issrng  20458  znval  21087  znle2  21109  evpmss  21139  psgnevpmb  21140  ptbasfi  23085  ptval2  23105  ptrescn  23143  xkoptsub  23158  qtopval  23199  txswaphmeolem  23308  ptcmpg  23561  tgplacthmeo  23607  trust  23734  prdsxmslem2  24038  metuval  24058  nghmfval  24239  isnghm  24240  pi1xfrcnv  24573  ismbf1  25141  ismbf  25145  mbfconst  25150  mbfres2  25162  cncombf  25175  deg1val  25614  fta1glem2  25684  fta1g  25685  fta1b  25687  dgrval  25742  dgrlem  25743  coe11  25767  fta1lem  25820  vieta1lem2  25824  ispth  29011  uhgrwkspthlem2  29042  usgr2wlkspthlem1  29045  usgr2wlkspthlem2  29046  pthdlem1  29054  2spthd  29226  3spthd  29460  f1o3d  31882  xppreima2  31907  ofpreima  31921  fcnvgreu  31929  mptiffisupp  31946  fpwrelmapffslem  31988  gsumhashmul  32239  tocycfv  32299  tocycf  32307  cycpm2tr  32309  cycpmconjvlem  32331  evpmval  32335  altgnsg  32339  irngval  32780  ordtrest2NEW  32934  qqhval  32985  indf1ofs  33055  esum2dlem  33121  mbfmcst  33289  omssubadd  33330  sitgfval  33371  eulerpartlemgf  33409  orvcval  33487  pthhashvtx  34149  cvmliftmolem1  34303  cvmliftlem5  34311  cvmliftlem15  34320  cvmlift2lem9a  34325  cvmlift2lem9  34333  ismfs  34571  mthmval  34597  wsuceq123  34817  bj-iminvval2  36123  cnambfre  36584  itg2addnclem2  36588  ftc1anclem1  36609  ftc1anclem6  36614  dfsymrels2  37463  dfsymrel2  37467  cdlemg1finvtrlemN  39494  tendoicbv  39712  tendoi  39713  tendoi2  39714  tendoicl  39715  docaffvalN  40040  docafvalN  40041  dihmeetlem1N  40209  dihglblem5apreN  40210  diophrw  41545  rmxfval  41690  rmyfval  41691  aomclem8  41851  cnvtrclfv  42523  frege131d  42563  dssmapnvod  42819  smfpimioo  45551  smfpimcc  45572  smfsuplem2  45576