Theorem cnveqd 5830

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-br 5086  df-opab 5148  df-cnv 5639

This theorem is referenced by:  opswap  6193  cores2  6224  fimacnvinrn  7023  nvocnv  7236  2ndval2  7960  2nd1st  7991  cnvf1olem  8060  fparlem3  8064  fparlem4  8065  brtpos2  8182  dftpos4  8195  tpostpos  8196  tposf12  8201  xpcomco  9005  infeq123d  9395  cantnffval2  9616  cnfcomlem  9620  fseqenlem2  9947  dfac12lem1  10066  dfac12r  10069  fpwwe2cbv  10553  fpwwe2lem2  10555  fpwwe2lem5  10558  fpwwe2lem8  10561  fpwwecbv  10567  fpwwelem  10568  funcnvs2  14875  funcnvs3  14876  funcnvs4  14877  relexpcnv  14997  fsumcnv  15735  fprodcnv  15948  bitsf1ocnv  16413  vdwpc  16951  imasval  17475  xpsval  17534  monfval  17699  ismon  17700  monpropd  17704  isepi  17707  invffval  17725  invfval  17726  dfiso2  17739  isofn  17742  oppcinv  17747  isfth  17883  catcisolem  18077  oduval  18254  oduleval  18255  gsumvalx  18644  grpinvcnv  18982  grplactcnv  19019  eqglact  19154  gsumcom2  19950  isunit  20353  issrng  20821  znval  21515  znle2  21533  evpmss  21566  psgnevpmb  21567  ptbasfi  23546  ptval2  23566  ptrescn  23604  xkoptsub  23619  qtopval  23660  txswaphmeolem  23769  ptcmpg  24022  tgplacthmeo  24068  trust  24194  prdsxmslem2  24494  metuval  24514  nghmfval  24687  isnghm  24688  pi1xfrcnv  25024  ismbf1  25591  ismbf  25595  mbfconst  25600  mbfres2  25612  cncombf  25625  deg1val  26061  fta1glem2  26134  fta1g  26135  fta1b  26137  dgrval  26193  dgrlem  26194  coe11  26218  fta1lem  26273  vieta1lem2  26277  ispth  29789  dfpth2  29797  uhgrwkspthlem2  29822  usgr2wlkspthlem1  29825  usgr2wlkspthlem2  29826  pthdlem1  29834  2spthd  30009  3spthd  30246  f1o3d  32699  xppreima2  32724  ofpreima  32738  fcnvgreu  32745  mptiffisupp  32766  fpwrelmapffslem  32805  indf1ofs  32926  gsumhashmul  33128  tocycfv  33170  tocycf  33178  cycpm2tr  33180  cycpmconjvlem  33202  evpmval  33206  altgnsg  33210  ply1dg3rt0irred  33644  vieta  33724  irngval  33829  ordtrest2NEW  34067  qqhval  34116  esum2dlem  34236  mbfmcst  34403  omssubadd  34444  sitgfval  34485  eulerpartlemgf  34523  orvcval  34602  pthhashvtx  35310  cvmliftmolem1  35463  cvmliftlem5  35471  cvmliftlem15  35480  cvmlift2lem9a  35485  cvmlift2lem9  35493  ismfs  35731  mthmval  35757  wsuceq123  35994  bj-iminvval2  37508  cnambfre  37989  itg2addnclem2  37993  ftc1anclem1  38014  ftc1anclem6  38019  dfsymrels2  38946  dfsymrel2  38954  cdlemg1finvtrlemN  41021  tendoicbv  41239  tendoi  41240  tendoi2  41241  tendoicl  41242  docaffvalN  41567  docafvalN  41568  dihmeetlem1N  41736  dihglblem5apreN  41737  diophrw  43191  rmxfval  43332  rmyfval  43333  aomclem8  43489  cnvtrclfv  44151  frege131d  44191  dssmapnvod  44447  smfpimioo  47215  smfpimcc  47236  smfsuplem2  47240  upgrimpths  48385  dftpos5  49349  tposideq  49363  invfn  49505  invpropdlem  49513  imaidfu  49585  idfth  49633  idsubc  49635  swapf1a  49744  swapf2a  49746  swapf1  49747  swapf2  49749