Theorem cnveqd 5865

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

Syntax hints:   → wi 4   = wceq 1568  ^◡ccnv 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-ss 3930  df-br 5115  df-opab 5179  df-cnv 5673

This theorem is referenced by:  csbcnv  5876  opswap  6234  cores2  6265  fimacnvinrn  7070  nvocnv  7283  2ndval2  8007  2nd1st  8038  cnvf1olem  8108  fparlem3  8112  fparlem4  8113  brtpos2  8231  dftpos4  8244  tpostpos  8245  tposf12  8250  xpcomco  9058  infeq123d  9445  cantnffval2  9667  cnfcomlem  9671  fseqenlem2  10012  dfac12lem1  10130  dfac12r  10133  fpwwe2cbv  10618  fpwwe2lem2  10620  fpwwe2lem5  10623  fpwwe2lem8  10626  fpwwecbv  10632  fpwwelem  10633  funcnvs2  14953  funcnvs3  14954  funcnvs4  14955  relexpcnv  15075  fsumcnv  15827  fprodcnv  16040  bitsf1ocnv  16505  vdwpc  17043  imasval  17568  xpsval  17627  monfval  17792  ismon  17793  monpropd  17797  isepi  17800  invffval  17818  invfval  17819  dfiso2  17832  isofn  17835  oppcinv  17840  isfth  17976  catcisolem  18170  oduval  18347  oduleval  18348  gsumvalx  18737  grpinvcnv  19076  grplactcnv  19112  eqglact  19250  gsumcom2  20048  isunit  20458  issrng  20930  znval  21668  znle2  21686  evpmss  21719  psgnevpmb  21720  ptbasfi  23721  ptval2  23741  ptrescn  23779  xkoptsub  23794  qtopval  23835  txswaphmeolem  23944  ptcmpg  24197  tgplacthmeo  24243  trust  24369  prdsxmslem2  24669  metuval  24689  nghmfval  24862  isnghm  24863  pi1xfrcnv  25199  ismbf1  25766  ismbf  25770  mbfconst  25775  mbfres2  25787  cncombf  25800  deg1val  26236  fta1glem2  26309  fta1g  26310  fta1b  26312  dgrval  26368  dgrlem  26369  coe11  26393  fta1lem  26451  vieta1lem2  26455  ispth  30040  dfpth2  30048  uhgrwkspthlem2  30073  usgr2wlkspthlem1  30076  usgr2wlkspthlem2  30077  pthdlem1  30085  2spthd  30260  3spthd  30497  f1o3d  32941  xppreima2  32966  ofpreima  32980  fcnvgreu  32987  mptiffisupp  33008  fpwrelmapffslem  33047  indf1ofs  33156  gsumhashmul  33357  tocycfv  33399  tocycf  33407  cycpm2tr  33409  cycpmconjvlem  33431  evpmval  33435  altgnsg  33439  ply1dg3rt0irred  33844  vieta  33940  irngval  34045  ordtrest2NEW  34283  qqhval  34332  esum2dlem  34452  mbfmcst  34619  omssubadd  34660  sitgfval  34701  eulerpartlemgf  34739  orvcval  34818  pthhashvtx  35578  cvmliftmolem1  35731  cvmliftlem5  35739  cvmliftlem15  35748  cvmlift2lem9a  35753  cvmlift2lem9  35761  ismfs  35999  mthmval  36025  wsuceq123  36262  bj-iminvval2  37786  cnambfre  38267  itg2addnclem2  38271  ftc1anclem1  38292  ftc1anclem6  38297  dfsymrels2  39224  dfsymrel2  39232  cdlemg1finvtrlemN  41299  tendoicbv  41517  tendoi  41518  tendoi2  41519  tendoicl  41520  docaffvalN  41845  docafvalN  41846  dihmeetlem1N  42014  dihglblem5apreN  42015  diophrw  43442  rmxfval  43583  rmyfval  43584  aomclem8  43740  cnvtrclfv  44402  frege131d  44442  dssmapnvod  44698  smfpimioo  47453  smfpimcc  47474  smfsuplem2  47478  upgrimpths  48623  dftpos5  49601  tposideq  49615  invfn  49757  invpropdlem  49765  imaidfu  49837  idfth  49885  idsubc  49887  swapf1a  49996  swapf2a  49998  swapf1  49999  swapf2  50001