Theorem cnveqd 5849

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

Syntax hints:   → wi 4   = wceq 1562  ^◡ccnv 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ss 3923  df-br 5103  df-opab 5165  df-cnv 5657

This theorem is referenced by:  csbcnv  5860  opswap  6218  cores2  6249  fimacnvinrn  7054  nvocnv  7267  2ndval2  7990  2nd1st  8021  cnvf1olem  8091  fparlem3  8095  fparlem4  8096  brtpos2  8214  dftpos4  8227  tpostpos  8228  tposf12  8233  xpcomco  9041  infeq123d  9430  cantnffval2  9652  cnfcomlem  9656  fseqenlem2  9983  dfac12lem1  10102  dfac12r  10105  fpwwe2cbv  10590  fpwwe2lem2  10592  fpwwe2lem5  10595  fpwwe2lem8  10598  fpwwecbv  10604  fpwwelem  10605  funcnvs2  14928  funcnvs3  14929  funcnvs4  14930  relexpcnv  15050  fsumcnv  15802  fprodcnv  16015  bitsf1ocnv  16480  vdwpc  17018  imasval  17543  xpsval  17602  monfval  17767  ismon  17768  monpropd  17772  isepi  17775  invffval  17793  invfval  17794  dfiso2  17807  isofn  17810  oppcinv  17815  isfth  17951  catcisolem  18145  oduval  18322  oduleval  18323  gsumvalx  18712  grpinvcnv  19050  grplactcnv  19087  eqglact  19222  gsumcom2  20017  isunit  20424  issrng  20895  znval  21589  znle2  21607  evpmss  21640  psgnevpmb  21641  ptbasfi  23643  ptval2  23663  ptrescn  23701  xkoptsub  23716  qtopval  23757  txswaphmeolem  23866  ptcmpg  24119  tgplacthmeo  24165  trust  24291  prdsxmslem2  24591  metuval  24611  nghmfval  24784  isnghm  24785  pi1xfrcnv  25121  ismbf1  25688  ismbf  25692  mbfconst  25697  mbfres2  25709  cncombf  25722  deg1val  26158  fta1glem2  26231  fta1g  26232  fta1b  26234  dgrval  26290  dgrlem  26291  coe11  26315  fta1lem  26373  vieta1lem2  26377  ispth  29923  dfpth2  29931  uhgrwkspthlem2  29956  usgr2wlkspthlem1  29959  usgr2wlkspthlem2  29960  pthdlem1  29968  2spthd  30143  3spthd  30380  f1o3d  32830  xppreima2  32855  ofpreima  32869  fcnvgreu  32876  mptiffisupp  32897  fpwrelmapffslem  32936  indf1ofs  33046  gsumhashmul  33249  tocycfv  33291  tocycf  33299  cycpm2tr  33301  cycpmconjvlem  33323  evpmval  33327  altgnsg  33331  ply1dg3rt0irred  33782  vieta  33879  irngval  33984  ordtrest2NEW  34222  qqhval  34271  esum2dlem  34391  mbfmcst  34558  omssubadd  34599  sitgfval  34640  eulerpartlemgf  34678  orvcval  34757  pthhashvtx  35483  cvmliftmolem1  35636  cvmliftlem5  35644  cvmliftlem15  35653  cvmlift2lem9a  35658  cvmlift2lem9  35666  ismfs  35904  mthmval  35930  wsuceq123  36167  bj-iminvval2  37691  cnambfre  38172  itg2addnclem2  38176  ftc1anclem1  38197  ftc1anclem6  38202  dfsymrels2  39129  dfsymrel2  39137  cdlemg1finvtrlemN  41204  tendoicbv  41422  tendoi  41423  tendoi2  41424  tendoicl  41425  docaffvalN  41750  docafvalN  41751  dihmeetlem1N  41919  dihglblem5apreN  41920  diophrw  43345  rmxfval  43486  rmyfval  43487  aomclem8  43643  cnvtrclfv  44305  frege131d  44345  dssmapnvod  44601  smfpimioo  47366  smfpimcc  47387  smfsuplem2  47391  upgrimpths  48536  dftpos5  49500  tposideq  49514  invfn  49656  invpropdlem  49664  imaidfu  49736  idfth  49784  idsubc  49786  swapf1a  49895  swapf2a  49897  swapf1  49898  swapf2  49900