Theorem coeq1d 5765

Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)

Hypothesis

Ref	Expression
coeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
coeq1d	⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Proof of Theorem coeq1d

Step	Hyp	Ref	Expression
1		coeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		coeq1 5761	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Syntax hints:   → wi 4   = wceq 1539   ∘ ccom 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3433  df-in 3895  df-ss 3905  df-br 5076  df-opab 5138  df-co 5595

This theorem is referenced by:  coeq12d  5768  fcof1oinvd  7159  domss2  8912  mapen  8917  mapfien  9156  hashfacen  14155  hashfacenOLD  14156  relexpsucnnr  14725  relexpsucnnl  14730  relexpsucr  14732  relexpsucrd  14733  relexpaddnn  14751  imasval  17211  cofuass  17593  cofulid  17594  setcinv  17794  catcisolem  17814  catciso  17815  yonedalem3b  17986  gsumvalx  18349  frmdup3lem  18494  symggrplem  18512  f1omvdco2  19045  symggen  19067  psgnunilem1  19090  gsumval3  19497  gsumzf1o  19502  znval  20728  znle2  20750  psrass1lemOLD  21132  psrass1lem  21135  coe1add  21424  evls1fval  21474  evl1sca  21489  evl1var  21491  evls1var  21493  pf1mpf  21507  pf1ind  21510  tcphds  24384  dvnfval  25075  hocsubdir  30134  fcoinver  30933  fcobij  31044  symgfcoeu  31338  symgcom  31339  pmtrcnel2  31346  tocyc01  31372  cycpm2tr  31373  cycpmconjv  31396  cycpmconjslem1  31408  cycpmconjslem2  31409  cycpmconjs  31410  cyc3conja  31411  reprpmtf1o  32593  hgt750lemg  32621  subfacp1lem5  33133  mrsubffval  33456  mrsubfval  33457  mrsubrn  33462  elmrsubrn  33469  upixp  35874  ltrncoidN  38129  trlcoat  38724  trlcone  38729  cdlemg47a  38735  cdlemg47  38737  ltrnco4  38740  tendovalco  38766  tendoplcbv  38776  tendopl  38777  tendoplass  38784  tendo0pl  38792  tendoipl  38798  cdlemk45  38948  cdlemk53b  38957  cdlemk55a  38960  erngdvlem3  38991  erngdvlem3-rN  38999  tendocnv  39022  dvhvaddcbv  39090  dvhvaddval  39091  dvhvaddass  39098  dicvscacl  39192  cdlemn8  39205  dihordlem7b  39216  dihopelvalcpre  39249  relexp2  41245  relexpxpnnidm  41271  relexpiidm  41272  relexpmulnn  41277  relexpaddss  41286  trclfvcom  41291  trclfvdecomr  41296  frege131d  41332  dssmap2d  41590  fundcmpsurbijinjpreimafv  44816  isomushgr  45235