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 5658

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3919  df-br 5108  df-opab 5172  df-cnv 5667

This theorem is used by:  csbcnv  5870  opswap  6229  cores2  6260  fimacnvinrn  7067  nvocnv  7285  2ndval2  8007  2nd1st  8038  cnvf1olem  8110  fparlem3  8114  fparlem4  8115  brtpos2  8233  dftpos4  8246  tpostpos  8247  tposf12  8252  xpcomco  9068  infeq123d  9455  cantnffval2  9677  cnfcomlem  9681  fseqenlem2  10031  dfac12lem1  10149  dfac12r  10152  fpwwe2cbv  10642  fpwwe2lem2  10644  fpwwe2lem5  10647  fpwwe2lem8  10650  fpwwecbv  10656  fpwwelem  10657  funcnvs2  14986  funcnvs3  14987  funcnvs4  14988  relexpcnv  15110  fsumcnv  15861  fprodcnv  16074  bitsf1ocnv  16538  vdwpc  17076  imasval  17601  xpsval  17660  monfval  17825  ismon  17826  monpropd  17830  isepi  17833  invffval  17851  invfval  17852  dfiso2  17865  isofn  17868  oppcinv  17873  isfth  18009  catcisolem  18203  oduval  18380  oduleval  18381  gsumvalx  18780  grpinvcnv  19131  grplactcnv  19167  eqglact  19305  gsumcom2  20103  isunit  20515  issrng  21011  znval  21749  znle2  21767  evpmss  21800  psgnevpmb  21801  ptbasfi  23808  ptval2  23828  ptrescn  23866  xkoptsub  23881  qtopval  23922  txswaphmeolem  24031  ptcmpg  24284  tgplacthmeo  24330  trust  24456  prdsxmslem2  24756  metuval  24776  nghmfval  24949  isnghm  24950  pi1xfrcnv  25286  ismbf1  25853  ismbf  25857  mbfconst  25862  mbfres2  25874  cncombf  25887  deg1val  26323  fta1glem2  26396  fta1g  26397  fta1b  26399  dgrval  26455  dgrlem  26456  coe11  26480  fta1lem  26538  vieta1lem2  26542  ispth  30171  dfpth2  30179  pthhashvtx  30180  uhgrwkspthlem2  30205  usgr2wlkspthlem1  30208  usgr2wlkspthlem2  30209  pthdlem1  30217  2spthd  30395  3spthd  30642  f1o3d  33086  xppreima2  33111  ofpreima  33125  fcnvgreu  33132  mptiffisupp  33152  fpwrelmapffslem  33190  indf1ofs  33299  gsumhashmul  33494  tocycfv  33536  tocycf  33544  cycpm2tr  33546  cycpmconjvlem  33568  evpmval  33572  altgnsg  33576  ply1dg3rt0irred  33981  vieta  34077  irngval  34182  ordtrest2NEW  34420  qqhval  34469  esum2dlem  34589  mbfmcst  34757  omssubadd  34798  sitgfval  34839  eulerpartlemgf  34877  orvcval  34956  cvmliftmolem1  35847  cvmliftlem5  35855  cvmliftlem15  35864  cvmlift2lem9a  35869  cvmlift2lem9  35877  ismfs  36115  mthmval  36141  wsuceq123  36378  bj-iminvval2  37933  cnambfre  38404  itg2addnclem2  38408  ftc1anclem1  38429  ftc1anclem6  38434  dfsymrels2  39360  dfsymrel2  39368  cdlemg1finvtrlemN  41435  tendoicbv  41653  tendoi  41654  tendoi2  41655  tendoicl  41656  docaffvalN  41981  docafvalN  41982  dihmeetlem1N  42150  dihglblem5apreN  42151  diophrw  43591  rmxfval  43732  rmyfval  43733  aomclem8  43889  cnvtrclfv  44551  frege131d  44591  dssmapnvod  44847  smfpimioo  47602  smfpimcc  47623  smfsuplem2  47627  upgrimpths  48812  dftpos5  49787  tposideq  49801  invfn  49943  invpropdlem  49951  imaidfu  50023  idfth  50071  idsubc  50073  swapf1a  50182  swapf2a  50184  swapf1  50185  swapf2  50187