Theorem cnveqd 5872

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

Syntax hints:   → wi 4   = wceq 1534  ^◡ccnv 5671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-in 3952  df-ss 3962  df-br 5143  df-opab 5205  df-cnv 5680

This theorem is referenced by:  opswap  6227  cores2  6257  fimacnvinrn  7075  nvocnv  7284  2ndval2  8005  2nd1st  8036  cnvf1olem  8109  fparlem3  8113  fparlem4  8114  brtpos2  8231  dftpos4  8244  tpostpos  8245  tposf12  8250  xpcomco  9080  infeq123d  9498  cantnffval2  9712  cnfcomlem  9716  fseqenlem2  10042  dfac12lem1  10160  dfac12r  10163  fpwwe2cbv  10647  fpwwe2lem2  10649  fpwwe2lem5  10652  fpwwe2lem8  10655  fpwwecbv  10661  fpwwelem  10662  funcnvs2  14890  funcnvs3  14891  funcnvs4  14892  relexpcnv  15008  fsumcnv  15745  fprodcnv  15953  bitsf1ocnv  16412  vdwpc  16942  imasval  17486  xpsval  17545  monfval  17708  ismon  17709  monpropd  17713  isepi  17716  invffval  17734  invfval  17735  dfiso2  17748  isofn  17751  oppcinv  17756  isfth  17896  catcisolem  18092  oduval  18273  oduleval  18274  gsumvalx  18629  grpinvcnv  18956  grplactcnv  18992  eqglact  19127  gsumcom2  19923  isunit  20305  issrng  20723  znval  21458  znle2  21480  evpmss  21511  psgnevpmb  21512  ptbasfi  23478  ptval2  23498  ptrescn  23536  xkoptsub  23551  qtopval  23592  txswaphmeolem  23701  ptcmpg  23954  tgplacthmeo  24000  trust  24127  prdsxmslem2  24431  metuval  24451  nghmfval  24632  isnghm  24633  pi1xfrcnv  24977  ismbf1  25546  ismbf  25550  mbfconst  25555  mbfres2  25567  cncombf  25580  deg1val  26025  fta1glem2  26096  fta1g  26097  fta1b  26099  dgrval  26155  dgrlem  26156  coe11  26180  fta1lem  26235  vieta1lem2  26239  ispth  29530  uhgrwkspthlem2  29561  usgr2wlkspthlem1  29564  usgr2wlkspthlem2  29565  pthdlem1  29573  2spthd  29745  3spthd  29979  f1o3d  32405  xppreima2  32430  ofpreima  32444  fcnvgreu  32452  mptiffisupp  32467  fpwrelmapffslem  32508  gsumhashmul  32764  tocycfv  32824  tocycf  32832  cycpm2tr  32834  cycpmconjvlem  32856  evpmval  32860  altgnsg  32864  irngval  33353  ordtrest2NEW  33518  qqhval  33569  indf1ofs  33639  esum2dlem  33705  mbfmcst  33873  omssubadd  33914  sitgfval  33955  eulerpartlemgf  33993  orvcval  34071  pthhashvtx  34731  cvmliftmolem1  34885  cvmliftlem5  34893  cvmliftlem15  34902  cvmlift2lem9a  34907  cvmlift2lem9  34915  ismfs  35153  mthmval  35179  wsuceq123  35404  bj-iminvval2  36667  cnambfre  37135  itg2addnclem2  37139  ftc1anclem1  37160  ftc1anclem6  37165  dfsymrels2  38011  dfsymrel2  38015  cdlemg1finvtrlemN  40042  tendoicbv  40260  tendoi  40261  tendoi2  40262  tendoicl  40263  docaffvalN  40588  docafvalN  40589  dihmeetlem1N  40757  dihglblem5apreN  40758  diophrw  42173  rmxfval  42318  rmyfval  42319  aomclem8  42479  cnvtrclfv  43148  frege131d  43188  dssmapnvod  43444  smfpimioo  46169  smfpimcc  46190  smfsuplem2  46194