Theorem cnveqd 5860

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ^◡ccnv 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921  df-br 5109  df-opab 5173  df-cnv 5668

This theorem is used by:  csbcnv  5871  opswap  6229  cores2  6260  fimacnvinrn  7066  nvocnv  7279  2ndval2  8002  2nd1st  8033  cnvf1olem  8103  fparlem3  8107  fparlem4  8108  brtpos2  8226  dftpos4  8239  tpostpos  8240  tposf12  8245  xpcomco  9053  infeq123d  9440  cantnffval2  9662  cnfcomlem  9666  fseqenlem2  10016  dfac12lem1  10134  dfac12r  10137  fpwwe2cbv  10621  fpwwe2lem2  10623  fpwwe2lem5  10626  fpwwe2lem8  10629  fpwwecbv  10635  fpwwelem  10636  funcnvs2  14957  funcnvs3  14958  funcnvs4  14959  relexpcnv  15079  fsumcnv  15831  fprodcnv  16044  bitsf1ocnv  16508  vdwpc  17046  imasval  17571  xpsval  17630  monfval  17795  ismon  17796  monpropd  17800  isepi  17803  invffval  17821  invfval  17822  dfiso2  17835  isofn  17838  oppcinv  17843  isfth  17979  catcisolem  18173  oduval  18350  oduleval  18351  gsumvalx  18740  grpinvcnv  19079  grplactcnv  19115  eqglact  19253  gsumcom2  20051  isunit  20462  issrng  20958  znval  21696  znle2  21714  evpmss  21747  psgnevpmb  21748  ptbasfi  23749  ptval2  23769  ptrescn  23807  xkoptsub  23822  qtopval  23863  txswaphmeolem  23972  ptcmpg  24225  tgplacthmeo  24271  trust  24397  prdsxmslem2  24697  metuval  24717  nghmfval  24890  isnghm  24891  pi1xfrcnv  25227  ismbf1  25794  ismbf  25798  mbfconst  25803  mbfres2  25815  cncombf  25828  deg1val  26264  fta1glem2  26337  fta1g  26338  fta1b  26340  dgrval  26396  dgrlem  26397  coe11  26421  fta1lem  26479  vieta1lem2  26483  ispth  30081  dfpth2  30089  uhgrwkspthlem2  30114  usgr2wlkspthlem1  30117  usgr2wlkspthlem2  30118  pthdlem1  30126  2spthd  30301  3spthd  30538  f1o3d  32982  xppreima2  33007  ofpreima  33021  fcnvgreu  33028  mptiffisupp  33049  fpwrelmapffslem  33088  indf1ofs  33197  gsumhashmul  33396  tocycfv  33438  tocycf  33446  cycpm2tr  33448  cycpmconjvlem  33470  evpmval  33474  altgnsg  33478  ply1dg3rt0irred  33883  vieta  33979  irngval  34084  ordtrest2NEW  34322  qqhval  34371  esum2dlem  34491  mbfmcst  34658  omssubadd  34699  sitgfval  34740  eulerpartlemgf  34778  orvcval  34857  pthhashvtx  35628  cvmliftmolem1  35781  cvmliftlem5  35789  cvmliftlem15  35798  cvmlift2lem9a  35803  cvmlift2lem9  35811  ismfs  36049  mthmval  36075  wsuceq123  36312  bj-iminvval2  37866  cnambfre  38347  itg2addnclem2  38351  ftc1anclem1  38372  ftc1anclem6  38377  dfsymrels2  39302  dfsymrel2  39310  cdlemg1finvtrlemN  41377  tendoicbv  41595  tendoi  41596  tendoi2  41597  tendoicl  41598  docaffvalN  41923  docafvalN  41924  dihmeetlem1N  42092  dihglblem5apreN  42093  diophrw  43518  rmxfval  43659  rmyfval  43660  aomclem8  43816  cnvtrclfv  44478  frege131d  44518  dssmapnvod  44774  smfpimioo  47529  smfpimcc  47550  smfsuplem2  47554  upgrimpths  48702  dftpos5  49680  tposideq  49694  invfn  49836  invpropdlem  49844  imaidfu  49916  idfth  49964  idsubc  49966  swapf1a  50075  swapf2a  50077  swapf1  50078  swapf2  50080