Theorem cnveqd 5900

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

Syntax hints:   → wi 4   = wceq 1537  ^◡ccnv 5699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-cnv 5708

This theorem is referenced by:  opswap  6260  cores2  6290  fimacnvinrn  7105  nvocnv  7317  2ndval2  8048  2nd1st  8079  cnvf1olem  8151  fparlem3  8155  fparlem4  8156  brtpos2  8273  dftpos4  8286  tpostpos  8287  tposf12  8292  xpcomco  9128  infeq123d  9550  cantnffval2  9764  cnfcomlem  9768  fseqenlem2  10094  dfac12lem1  10213  dfac12r  10216  fpwwe2cbv  10699  fpwwe2lem2  10701  fpwwe2lem5  10704  fpwwe2lem8  10707  fpwwecbv  10713  fpwwelem  10714  funcnvs2  14962  funcnvs3  14963  funcnvs4  14964  relexpcnv  15084  fsumcnv  15821  fprodcnv  16031  bitsf1ocnv  16490  vdwpc  17027  imasval  17571  xpsval  17630  monfval  17793  ismon  17794  monpropd  17798  isepi  17801  invffval  17819  invfval  17820  dfiso2  17833  isofn  17836  oppcinv  17841  isfth  17981  catcisolem  18177  oduval  18358  oduleval  18359  gsumvalx  18714  grpinvcnv  19046  grplactcnv  19083  eqglact  19219  gsumcom2  20017  isunit  20399  issrng  20867  znval  21573  znle2  21595  evpmss  21627  psgnevpmb  21628  ptbasfi  23610  ptval2  23630  ptrescn  23668  xkoptsub  23683  qtopval  23724  txswaphmeolem  23833  ptcmpg  24086  tgplacthmeo  24132  trust  24259  prdsxmslem2  24563  metuval  24583  nghmfval  24764  isnghm  24765  pi1xfrcnv  25109  ismbf1  25678  ismbf  25682  mbfconst  25687  mbfres2  25699  cncombf  25712  deg1val  26155  fta1glem2  26228  fta1g  26229  fta1b  26231  dgrval  26287  dgrlem  26288  coe11  26312  fta1lem  26367  vieta1lem2  26371  ispth  29759  uhgrwkspthlem2  29790  usgr2wlkspthlem1  29793  usgr2wlkspthlem2  29794  pthdlem1  29802  2spthd  29974  3spthd  30208  f1o3d  32646  xppreima2  32669  ofpreima  32683  fcnvgreu  32691  mptiffisupp  32705  fpwrelmapffslem  32746  gsumhashmul  33040  tocycfv  33102  tocycf  33110  cycpm2tr  33112  cycpmconjvlem  33134  evpmval  33138  altgnsg  33142  ply1dg3rt0irred  33572  irngval  33685  ordtrest2NEW  33869  qqhval  33920  indf1ofs  33990  esum2dlem  34056  mbfmcst  34224  omssubadd  34265  sitgfval  34306  eulerpartlemgf  34344  orvcval  34422  pthhashvtx  35095  cvmliftmolem1  35249  cvmliftlem5  35257  cvmliftlem15  35266  cvmlift2lem9a  35271  cvmlift2lem9  35279  ismfs  35517  mthmval  35543  wsuceq123  35778  bj-iminvval2  37160  cnambfre  37628  itg2addnclem2  37632  ftc1anclem1  37653  ftc1anclem6  37658  dfsymrels2  38501  dfsymrel2  38505  cdlemg1finvtrlemN  40532  tendoicbv  40750  tendoi  40751  tendoi2  40752  tendoicl  40753  docaffvalN  41078  docafvalN  41079  dihmeetlem1N  41247  dihglblem5apreN  41248  diophrw  42715  rmxfval  42860  rmyfval  42861  aomclem8  43018  cnvtrclfv  43686  frege131d  43726  dssmapnvod  43982  smfpimioo  46708  smfpimcc  46729  smfsuplem2  46733