Theorem cnveqd 5830

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-br 5103  df-opab 5165  df-cnv 5639

This theorem is referenced by:  opswap  6191  cores2  6221  fimacnvinrn  7026  nvocnv  7239  2ndval2  7966  2nd1st  7997  cnvf1olem  8067  fparlem3  8071  fparlem4  8072  brtpos2  8189  dftpos4  8202  tpostpos  8203  tposf12  8208  xpcomco  9009  infeq123d  9410  cantnffval2  9627  cnfcomlem  9631  fseqenlem2  9957  dfac12lem1  10076  dfac12r  10079  fpwwe2cbv  10562  fpwwe2lem2  10564  fpwwe2lem5  10567  fpwwe2lem8  10570  fpwwecbv  10576  fpwwelem  10577  funcnvs2  14857  funcnvs3  14858  funcnvs4  14859  relexpcnv  14979  fsumcnv  15717  fprodcnv  15927  bitsf1ocnv  16392  vdwpc  16929  imasval  17452  xpsval  17511  monfval  17676  ismon  17677  monpropd  17681  isepi  17684  invffval  17702  invfval  17703  dfiso2  17716  isofn  17719  oppcinv  17724  isfth  17860  catcisolem  18054  oduval  18231  oduleval  18232  gsumvalx  18587  grpinvcnv  18922  grplactcnv  18959  eqglact  19095  gsumcom2  19891  isunit  20295  issrng  20766  znval  21479  znle2  21497  evpmss  21530  psgnevpmb  21531  ptbasfi  23503  ptval2  23523  ptrescn  23561  xkoptsub  23576  qtopval  23617  txswaphmeolem  23726  ptcmpg  23979  tgplacthmeo  24025  trust  24152  prdsxmslem2  24452  metuval  24472  nghmfval  24645  isnghm  24646  pi1xfrcnv  24992  ismbf1  25560  ismbf  25564  mbfconst  25569  mbfres2  25581  cncombf  25594  deg1val  26036  fta1glem2  26109  fta1g  26110  fta1b  26112  dgrval  26168  dgrlem  26169  coe11  26193  fta1lem  26250  vieta1lem2  26254  ispth  29703  dfpth2  29711  uhgrwkspthlem2  29736  usgr2wlkspthlem1  29739  usgr2wlkspthlem2  29740  pthdlem1  29748  2spthd  29923  3spthd  30157  f1o3d  32603  xppreima2  32627  ofpreima  32641  fcnvgreu  32649  mptiffisupp  32668  fpwrelmapffslem  32707  indf1ofs  32841  gsumhashmul  33046  tocycfv  33083  tocycf  33091  cycpm2tr  33093  cycpmconjvlem  33115  evpmval  33119  altgnsg  33123  ply1dg3rt0irred  33546  irngval  33675  ordtrest2NEW  33908  qqhval  33957  esum2dlem  34077  mbfmcst  34245  omssubadd  34286  sitgfval  34327  eulerpartlemgf  34365  orvcval  34444  pthhashvtx  35110  cvmliftmolem1  35263  cvmliftlem5  35271  cvmliftlem15  35280  cvmlift2lem9a  35285  cvmlift2lem9  35293  ismfs  35531  mthmval  35557  wsuceq123  35797  bj-iminvval2  37177  cnambfre  37657  itg2addnclem2  37661  ftc1anclem1  37682  ftc1anclem6  37687  dfsymrels2  38531  dfsymrel2  38535  cdlemg1finvtrlemN  40564  tendoicbv  40782  tendoi  40783  tendoi2  40784  tendoicl  40785  docaffvalN  41110  docafvalN  41111  dihmeetlem1N  41279  dihglblem5apreN  41280  diophrw  42742  rmxfval  42887  rmyfval  42888  aomclem8  43045  cnvtrclfv  43708  frege131d  43748  dssmapnvod  44004  smfpimioo  46780  smfpimcc  46801  smfsuplem2  46805  upgrimpths  47904  dftpos5  48857  tposideq  48871  invfn  49014  invpropdlem  49022  imaidfu  49094  idfth  49142  idsubc  49144  swapf1a  49253  swapf2a  49255  swapf1  49256  swapf2  49258