Theorem cnveqd 5823

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ss 3917  df-br 5098  df-opab 5160  df-cnv 5631

This theorem is referenced by:  opswap  6186  cores2  6217  fimacnvinrn  7016  nvocnv  7227  2ndval2  7951  2nd1st  7982  cnvf1olem  8052  fparlem3  8056  fparlem4  8057  brtpos2  8174  dftpos4  8187  tpostpos  8188  tposf12  8193  xpcomco  8997  infeq123d  9387  cantnffval2  9606  cnfcomlem  9610  fseqenlem2  9937  dfac12lem1  10056  dfac12r  10059  fpwwe2cbv  10543  fpwwe2lem2  10545  fpwwe2lem5  10548  fpwwe2lem8  10551  fpwwecbv  10557  fpwwelem  10558  funcnvs2  14838  funcnvs3  14839  funcnvs4  14840  relexpcnv  14960  fsumcnv  15698  fprodcnv  15908  bitsf1ocnv  16373  vdwpc  16910  imasval  17434  xpsval  17493  monfval  17658  ismon  17659  monpropd  17663  isepi  17666  invffval  17684  invfval  17685  dfiso2  17698  isofn  17701  oppcinv  17706  isfth  17842  catcisolem  18036  oduval  18213  oduleval  18214  gsumvalx  18603  grpinvcnv  18938  grplactcnv  18975  eqglact  19110  gsumcom2  19906  isunit  20311  issrng  20779  znval  21492  znle2  21510  evpmss  21543  psgnevpmb  21544  ptbasfi  23527  ptval2  23547  ptrescn  23585  xkoptsub  23600  qtopval  23641  txswaphmeolem  23750  ptcmpg  24003  tgplacthmeo  24049  trust  24175  prdsxmslem2  24475  metuval  24495  nghmfval  24668  isnghm  24669  pi1xfrcnv  25015  ismbf1  25583  ismbf  25587  mbfconst  25592  mbfres2  25604  cncombf  25617  deg1val  26059  fta1glem2  26132  fta1g  26133  fta1b  26135  dgrval  26191  dgrlem  26192  coe11  26216  fta1lem  26273  vieta1lem2  26277  ispth  29775  dfpth2  29783  uhgrwkspthlem2  29808  usgr2wlkspthlem1  29811  usgr2wlkspthlem2  29812  pthdlem1  29820  2spthd  29995  3spthd  30232  f1o3d  32684  xppreima2  32709  ofpreima  32723  fcnvgreu  32730  mptiffisupp  32751  fpwrelmapffslem  32790  indf1ofs  32927  gsumhashmul  33129  tocycfv  33170  tocycf  33178  cycpm2tr  33180  cycpmconjvlem  33202  evpmval  33206  altgnsg  33210  ply1dg3rt0irred  33644  vieta  33715  irngval  33821  ordtrest2NEW  34059  qqhval  34108  esum2dlem  34228  mbfmcst  34395  omssubadd  34436  sitgfval  34477  eulerpartlemgf  34515  orvcval  34594  pthhashvtx  35301  cvmliftmolem1  35454  cvmliftlem5  35462  cvmliftlem15  35471  cvmlift2lem9a  35476  cvmlift2lem9  35484  ismfs  35722  mthmval  35748  wsuceq123  35985  bj-iminvval2  37368  cnambfre  37838  itg2addnclem2  37842  ftc1anclem1  37863  ftc1anclem6  37868  dfsymrels2  38795  dfsymrel2  38803  cdlemg1finvtrlemN  40870  tendoicbv  41088  tendoi  41089  tendoi2  41090  tendoicl  41091  docaffvalN  41416  docafvalN  41417  dihmeetlem1N  41585  dihglblem5apreN  41586  diophrw  43038  rmxfval  43183  rmyfval  43184  aomclem8  43340  cnvtrclfv  44002  frege131d  44042  dssmapnvod  44298  smfpimioo  47068  smfpimcc  47089  smfsuplem2  47093  upgrimpths  48192  dftpos5  49156  tposideq  49170  invfn  49312  invpropdlem  49320  imaidfu  49392  idfth  49440  idsubc  49442  swapf1a  49551  swapf2a  49553  swapf1  49554  swapf2  49556