Theorem cnveqd 5814

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

Syntax hints:   → wi 4   = wceq 1541  ^◡ccnv 5613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914  df-br 5090  df-opab 5152  df-cnv 5622

This theorem is referenced by:  opswap  6176  cores2  6207  fimacnvinrn  7004  nvocnv  7215  2ndval2  7939  2nd1st  7970  cnvf1olem  8040  fparlem3  8044  fparlem4  8045  brtpos2  8162  dftpos4  8175  tpostpos  8176  tposf12  8181  xpcomco  8980  infeq123d  9366  cantnffval2  9585  cnfcomlem  9589  fseqenlem2  9916  dfac12lem1  10035  dfac12r  10038  fpwwe2cbv  10521  fpwwe2lem2  10523  fpwwe2lem5  10526  fpwwe2lem8  10529  fpwwecbv  10535  fpwwelem  10536  funcnvs2  14820  funcnvs3  14821  funcnvs4  14822  relexpcnv  14942  fsumcnv  15680  fprodcnv  15890  bitsf1ocnv  16355  vdwpc  16892  imasval  17415  xpsval  17474  monfval  17639  ismon  17640  monpropd  17644  isepi  17647  invffval  17665  invfval  17666  dfiso2  17679  isofn  17682  oppcinv  17687  isfth  17823  catcisolem  18017  oduval  18194  oduleval  18195  gsumvalx  18584  grpinvcnv  18919  grplactcnv  18956  eqglact  19091  gsumcom2  19887  isunit  20291  issrng  20759  znval  21472  znle2  21490  evpmss  21523  psgnevpmb  21524  ptbasfi  23496  ptval2  23516  ptrescn  23554  xkoptsub  23569  qtopval  23610  txswaphmeolem  23719  ptcmpg  23972  tgplacthmeo  24018  trust  24144  prdsxmslem2  24444  metuval  24464  nghmfval  24637  isnghm  24638  pi1xfrcnv  24984  ismbf1  25552  ismbf  25556  mbfconst  25561  mbfres2  25573  cncombf  25586  deg1val  26028  fta1glem2  26101  fta1g  26102  fta1b  26104  dgrval  26160  dgrlem  26161  coe11  26185  fta1lem  26242  vieta1lem2  26246  ispth  29699  dfpth2  29707  uhgrwkspthlem2  29732  usgr2wlkspthlem1  29735  usgr2wlkspthlem2  29736  pthdlem1  29744  2spthd  29919  3spthd  30156  f1o3d  32608  xppreima2  32633  ofpreima  32647  fcnvgreu  32655  mptiffisupp  32674  fpwrelmapffslem  32715  indf1ofs  32847  gsumhashmul  33041  tocycfv  33078  tocycf  33086  cycpm2tr  33088  cycpmconjvlem  33110  evpmval  33114  altgnsg  33118  ply1dg3rt0irred  33546  irngval  33698  ordtrest2NEW  33936  qqhval  33985  esum2dlem  34105  mbfmcst  34272  omssubadd  34313  sitgfval  34354  eulerpartlemgf  34392  orvcval  34471  pthhashvtx  35172  cvmliftmolem1  35325  cvmliftlem5  35333  cvmliftlem15  35342  cvmlift2lem9a  35347  cvmlift2lem9  35355  ismfs  35593  mthmval  35619  wsuceq123  35856  bj-iminvval2  37238  cnambfre  37707  itg2addnclem2  37711  ftc1anclem1  37732  ftc1anclem6  37737  dfsymrels2  38636  dfsymrel2  38644  cdlemg1finvtrlemN  40673  tendoicbv  40891  tendoi  40892  tendoi2  40893  tendoicl  40894  docaffvalN  41219  docafvalN  41220  dihmeetlem1N  41388  dihglblem5apreN  41389  diophrw  42851  rmxfval  42996  rmyfval  42997  aomclem8  43153  cnvtrclfv  43816  frege131d  43856  dssmapnvod  44112  smfpimioo  46884  smfpimcc  46905  smfsuplem2  46909  upgrimpths  48008  dftpos5  48973  tposideq  48987  invfn  49130  invpropdlem  49138  imaidfu  49210  idfth  49258  idsubc  49260  swapf1a  49369  swapf2a  49371  swapf1  49372  swapf2  49374