Theorem cnveqd 5834

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-br 5101  df-opab 5163  df-cnv 5642

This theorem is referenced by:  opswap  6197  cores2  6228  fimacnvinrn  7027  nvocnv  7239  2ndval2  7963  2nd1st  7994  cnvf1olem  8064  fparlem3  8068  fparlem4  8069  brtpos2  8186  dftpos4  8199  tpostpos  8200  tposf12  8205  xpcomco  9009  infeq123d  9399  cantnffval2  9618  cnfcomlem  9622  fseqenlem2  9949  dfac12lem1  10068  dfac12r  10071  fpwwe2cbv  10555  fpwwe2lem2  10557  fpwwe2lem5  10560  fpwwe2lem8  10563  fpwwecbv  10569  fpwwelem  10570  funcnvs2  14850  funcnvs3  14851  funcnvs4  14852  relexpcnv  14972  fsumcnv  15710  fprodcnv  15920  bitsf1ocnv  16385  vdwpc  16922  imasval  17446  xpsval  17505  monfval  17670  ismon  17671  monpropd  17675  isepi  17678  invffval  17696  invfval  17697  dfiso2  17710  isofn  17713  oppcinv  17718  isfth  17854  catcisolem  18048  oduval  18225  oduleval  18226  gsumvalx  18615  grpinvcnv  18953  grplactcnv  18990  eqglact  19125  gsumcom2  19921  isunit  20326  issrng  20794  znval  21507  znle2  21525  evpmss  21558  psgnevpmb  21559  ptbasfi  23542  ptval2  23562  ptrescn  23600  xkoptsub  23615  qtopval  23656  txswaphmeolem  23765  ptcmpg  24018  tgplacthmeo  24064  trust  24190  prdsxmslem2  24490  metuval  24510  nghmfval  24683  isnghm  24684  pi1xfrcnv  25030  ismbf1  25598  ismbf  25602  mbfconst  25607  mbfres2  25619  cncombf  25632  deg1val  26074  fta1glem2  26147  fta1g  26148  fta1b  26150  dgrval  26206  dgrlem  26207  coe11  26231  fta1lem  26288  vieta1lem2  26292  ispth  29812  dfpth2  29820  uhgrwkspthlem2  29845  usgr2wlkspthlem1  29848  usgr2wlkspthlem2  29849  pthdlem1  29857  2spthd  30032  3spthd  30269  f1o3d  32722  xppreima2  32747  ofpreima  32761  fcnvgreu  32768  mptiffisupp  32789  fpwrelmapffslem  32828  indf1ofs  32965  gsumhashmul  33167  tocycfv  33209  tocycf  33217  cycpm2tr  33219  cycpmconjvlem  33241  evpmval  33245  altgnsg  33249  ply1dg3rt0irred  33683  vieta  33763  irngval  33869  ordtrest2NEW  34107  qqhval  34156  esum2dlem  34276  mbfmcst  34443  omssubadd  34484  sitgfval  34525  eulerpartlemgf  34563  orvcval  34642  pthhashvtx  35350  cvmliftmolem1  35503  cvmliftlem5  35511  cvmliftlem15  35520  cvmlift2lem9a  35525  cvmlift2lem9  35533  ismfs  35771  mthmval  35797  wsuceq123  36034  bj-iminvval2  37476  cnambfre  37948  itg2addnclem2  37952  ftc1anclem1  37973  ftc1anclem6  37978  dfsymrels2  38905  dfsymrel2  38913  cdlemg1finvtrlemN  40980  tendoicbv  41198  tendoi  41199  tendoi2  41200  tendoicl  41201  docaffvalN  41526  docafvalN  41527  dihmeetlem1N  41695  dihglblem5apreN  41696  diophrw  43145  rmxfval  43290  rmyfval  43291  aomclem8  43447  cnvtrclfv  44109  frege131d  44149  dssmapnvod  44405  smfpimioo  47174  smfpimcc  47195  smfsuplem2  47199  upgrimpths  48298  dftpos5  49262  tposideq  49276  invfn  49418  invpropdlem  49426  imaidfu  49498  idfth  49546  idsubc  49548  swapf1a  49657  swapf2a  49659  swapf1  49660  swapf2  49662