Theorem cnveqd 5859

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ^◡ccnv 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5107  df-opab 5171  df-cnv 5663

This theorem is used by:  csbcnv  5870  opswap  6242  cores2  6273  fimacnvinrn  7092  nvocnv  7309  2ndval2  8040  2nd1st  8070  cnvf1olem  8145  fparlem3  8149  fparlem4  8150  brtpos2  8274  dftpos4  8287  tpostpos  8288  tposf12  8293  xpcomco  9111  infeq123d  9498  cantnffval2  9720  cnfcomlem  9724  fseqenlem2  10128  dfac12lem1  10246  dfac12r  10249  fpwwe2cbv  10739  fpwwe2lem2  10741  fpwwe2lem5  10744  fpwwe2lem8  10747  fpwwecbv  10753  fpwwelem  10754  funcnvs2  15090  funcnvs3  15091  funcnvs4  15092  relexpcnv  15214  fsumcnv  15965  fprodcnv  16176  bitsf1ocnv  16640  vdwpc  17184  imasval  17709  xpsval  17768  monfval  17933  ismon  17934  monpropd  17938  isepi  17941  invffval  17959  invfval  17960  dfiso2  17973  isofn  17976  oppcinv  17981  isfth  18117  catcisolem  18311  oduval  18488  oduleval  18489  gsumvalx  18891  grpinvcnv  19243  grplactcnv  19279  eqglact  19417  gsumcom2  20216  isunit  20630  issrng  21128  znval  21868  znle2  21886  evpmss  21919  psgnevpmb  21920  ptbasfi  23927  ptval2  23947  ptrescn  23985  xkoptsub  24000  qtopval  24041  txswaphmeolem  24150  ptcmpg  24403  tgplacthmeo  24449  trust  24575  prdsxmslem2  24875  metuval  24895  nghmfval  25068  isnghm  25069  pi1xfrcnv  25405  ismbf1  25972  ismbf  25976  mbfconst  25981  mbfres2  25993  cncombf  26006  deg1val  26441  fta1glem2  26514  fta1g  26515  fta1b  26517  dgrval  26574  dgrlem  26575  coe11  26599  fta1lem  26655  vieta1lem2  26661  ispth  30333  dfpth2  30341  pthhashvtx  30342  uhgrwkspthlem2  30367  usgr2wlkspthlem1  30370  usgr2wlkspthlem2  30371  pthdlem1  30379  2spthd  30557  3spthd  30804  f1o3d  33289  xppreima2  33314  ofpreima  33328  fcnvgreu  33335  mptiffisupp  33354  fpwrelmapffslem  33391  indf1ofs  33500  gsumhashmul  33695  tocycfv  33737  tocycf  33745  cycpm2tr  33747  cycpmconjvlem  33769  evpmval  33773  altgnsg  33777  ply1dg3rt0irred  34183  vieta  34279  irngval  34384  ordtrest2NEW  34622  qqhval  34671  esum2dlem  34791  mbfmcst  34958  omssubadd  34999  sitgfval  35040  eulerpartlemgf  35078  orvcval  35157  cvmliftmolem1  36212  cvmliftlem5  36220  cvmliftlem15  36229  cvmlift2lem9a  36234  cvmlift2lem9  36242  ismfs  36480  mthmval  36506  wsuceq123  36753  bj-iminvval2  38306  cnambfre  38777  itg2addnclem2  38781  ftc1anclem1  38802  ftc1anclem6  38807  dfsymrels2  39748  dfsymrel2  39756  cdlemg1finvtrlemN  41823  tendoicbv  42041  tendoi  42042  tendoi2  42043  tendoicl  42044  docaffvalN  42369  docafvalN  42370  dihmeetlem1N  42538  dihglblem5apreN  42539  diophrw  43961  rmxfval  44102  rmyfval  44103  aomclem8  44254  cnvtrclfv  44914  frege131d  44954  dssmapnvod  45210  smfpimioo  48000  smfpimcc  48021  smfsuplem2  48025  upgrimpths  49210  dftpos5  50190  tposideq  50204  invfn  50347  invpropdlem  50355  imaidfu  50429  idfth  50477  idsubc  50479  swapf1a  50594  swapf2a  50596  swapf1  50597  swapf2  50599