Theorem cnveqd 5855

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-br 5120  df-opab 5182  df-cnv 5662

This theorem is referenced by:  opswap  6218  cores2  6248  fimacnvinrn  7060  nvocnv  7273  2ndval2  8004  2nd1st  8035  cnvf1olem  8107  fparlem3  8111  fparlem4  8112  brtpos2  8229  dftpos4  8242  tpostpos  8243  tposf12  8248  xpcomco  9074  infeq123d  9492  cantnffval2  9707  cnfcomlem  9711  fseqenlem2  10037  dfac12lem1  10156  dfac12r  10159  fpwwe2cbv  10642  fpwwe2lem2  10644  fpwwe2lem5  10647  fpwwe2lem8  10650  fpwwecbv  10656  fpwwelem  10657  funcnvs2  14930  funcnvs3  14931  funcnvs4  14932  relexpcnv  15052  fsumcnv  15787  fprodcnv  15997  bitsf1ocnv  16461  vdwpc  16998  imasval  17523  xpsval  17582  monfval  17743  ismon  17744  monpropd  17748  isepi  17751  invffval  17769  invfval  17770  dfiso2  17783  isofn  17786  oppcinv  17791  isfth  17927  catcisolem  18121  oduval  18298  oduleval  18299  gsumvalx  18652  grpinvcnv  18987  grplactcnv  19024  eqglact  19160  gsumcom2  19954  isunit  20331  issrng  20802  znval  21494  znle2  21512  evpmss  21544  psgnevpmb  21545  ptbasfi  23517  ptval2  23537  ptrescn  23575  xkoptsub  23590  qtopval  23631  txswaphmeolem  23740  ptcmpg  23993  tgplacthmeo  24039  trust  24166  prdsxmslem2  24466  metuval  24486  nghmfval  24659  isnghm  24660  pi1xfrcnv  25006  ismbf1  25575  ismbf  25579  mbfconst  25584  mbfres2  25596  cncombf  25609  deg1val  26051  fta1glem2  26124  fta1g  26125  fta1b  26127  dgrval  26183  dgrlem  26184  coe11  26208  fta1lem  26265  vieta1lem2  26269  ispth  29649  dfpth2  29657  uhgrwkspthlem2  29682  usgr2wlkspthlem1  29685  usgr2wlkspthlem2  29686  pthdlem1  29694  2spthd  29869  3spthd  30103  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  33541  irngval  33672  ordtrest2NEW  33900  qqhval  33949  esum2dlem  34069  mbfmcst  34237  omssubadd  34278  sitgfval  34319  eulerpartlemgf  34357  orvcval  34436  pthhashvtx  35096  cvmliftmolem1  35249  cvmliftlem5  35257  cvmliftlem15  35266  cvmlift2lem9a  35271  cvmlift2lem9  35279  ismfs  35517  mthmval  35543  wsuceq123  35778  bj-iminvval2  37158  cnambfre  37638  itg2addnclem2  37642  ftc1anclem1  37663  ftc1anclem6  37668  dfsymrels2  38509  dfsymrel2  38513  cdlemg1finvtrlemN  40540  tendoicbv  40758  tendoi  40759  tendoi2  40760  tendoicl  40761  docaffvalN  41086  docafvalN  41087  dihmeetlem1N  41255  dihglblem5apreN  41256  diophrw  42729  rmxfval  42874  rmyfval  42875  aomclem8  43032  cnvtrclfv  43695  frege131d  43735  dssmapnvod  43991  smfpimioo  46764  smfpimcc  46785  smfsuplem2  46789  upgrimpths  47870  dftpos5  48797  tposideq  48811  invfn  48948  invpropdlem  48953  imaidfu  49017  idfth  49046  idsubc  49047  swapf1a  49134  swapf2a  49136  swapf1  49137  swapf2  49139