Theorem cnveqd 5773

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

Syntax hints:   → wi 4   = wceq 1539  ^◡ccnv 5579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071  df-opab 5133  df-cnv 5588

This theorem is referenced by:  opswap  6121  cores2  6152  fimacnvinrn  6931  nvocnv  7134  2ndval2  7822  2nd1st  7852  cnvf1olem  7921  fparlem3  7925  fparlem4  7926  brtpos2  8019  dftpos4  8032  tpostpos  8033  tposf12  8038  xpcomco  8802  infeq123d  9170  cantnffval2  9383  cnfcomlem  9387  fseqenlem2  9712  dfac12lem1  9830  dfac12r  9833  fpwwe2cbv  10317  fpwwe2lem2  10319  fpwwe2lem5  10322  fpwwe2lem8  10325  fpwwecbv  10331  fpwwelem  10332  funcnvs2  14554  funcnvs3  14555  funcnvs4  14556  relexpcnv  14674  fsumcnv  15413  fprodcnv  15621  bitsf1ocnv  16079  vdwpc  16609  imasval  17139  xpsval  17198  monfval  17361  ismon  17362  monpropd  17366  isepi  17369  invffval  17387  invfval  17388  dfiso2  17401  isofn  17404  oppcinv  17409  isfth  17546  catcisolem  17741  oduval  17922  oduleval  17923  gsumvalx  18275  grpinvcnv  18558  grplactcnv  18593  eqglact  18722  gsumcom2  19491  isunit  19814  issrng  20025  znval  20651  znle2  20673  evpmss  20703  psgnevpmb  20704  ptbasfi  22640  ptval2  22660  ptrescn  22698  xkoptsub  22713  qtopval  22754  txswaphmeolem  22863  ptcmpg  23116  tgplacthmeo  23162  trust  23289  prdsxmslem2  23591  metuval  23611  nghmfval  23792  isnghm  23793  pi1xfrcnv  24126  ismbf1  24693  ismbf  24697  mbfconst  24702  mbfres2  24714  cncombf  24727  deg1val  25166  fta1glem2  25236  fta1g  25237  fta1b  25239  dgrval  25294  dgrlem  25295  coe11  25319  fta1lem  25372  vieta1lem2  25376  ispth  27992  uhgrwkspthlem2  28023  usgr2wlkspthlem1  28026  usgr2wlkspthlem2  28027  pthdlem1  28035  2spthd  28207  3spthd  28441  f1o3d  30863  xppreima2  30889  ofpreima  30904  fcnvgreu  30912  fpwrelmapffslem  30969  gsumhashmul  31218  tocycfv  31278  tocycf  31286  cycpm2tr  31288  cycpmconjvlem  31310  evpmval  31314  altgnsg  31318  ordtrest2NEW  31775  qqhval  31824  indf1ofs  31894  esum2dlem  31960  mbfmcst  32126  omssubadd  32167  sitgfval  32208  eulerpartlemgf  32246  orvcval  32324  pthhashvtx  32989  cvmliftmolem1  33143  cvmliftlem5  33151  cvmliftlem15  33160  cvmlift2lem9a  33165  cvmlift2lem9  33173  ismfs  33411  mthmval  33437  wsuceq123  33735  bj-iminvval2  35292  cnambfre  35752  itg2addnclem2  35756  ftc1anclem1  35777  ftc1anclem6  35782  dfsymrels2  36586  dfsymrel2  36590  cdlemg1finvtrlemN  38516  tendoicbv  38734  tendoi  38735  tendoi2  38736  tendoicl  38737  docaffvalN  39062  docafvalN  39063  dihmeetlem1N  39231  dihglblem5apreN  39232  diophrw  40497  rmxfval  40642  rmyfval  40643  aomclem8  40802  cnvtrclfv  41221  frege131d  41261  dssmapnvod  41517  smfpimioo  44208  smfpimcc  44228  smfsuplem2  44232