Theorem coeq1d 5810

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

Syntax hints:   → wi 4   = wceq 1542   ∘ ccom 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-br 5087  df-opab 5149  df-co 5633

This theorem is referenced by:  coeq12d  5813  fcof1oinvd  7241  domss2  9067  mapen  9072  mapfien  9314  hashfacen  14407  relexpsucnnr  14978  relexpsucnnl  14983  relexpsucr  14985  relexpsucrd  14986  relexpaddnn  15004  imasval  17466  cofuass  17847  cofulid  17848  setcinv  18048  catcisolem  18068  catciso  18069  yonedalem3b  18236  gsumvalx  18635  frmdup3lem  18825  symggrplem  18843  f1omvdco2  19414  symggen  19436  psgnunilem1  19459  gsumval3  19873  gsumzf1o  19878  znval  21525  znle2  21543  psrass1lem  21922  coe1add  22239  evls1fval  22294  evl1sca  22309  evl1var  22311  evls1var  22313  pf1mpf  22327  pf1ind  22330  tcphds  25208  dvnfval  25899  hocsubdir  31871  fcoinver  32689  fcobij  32808  cocnvf1o  32817  ccatws1f1olast  33027  symgfcoeu  33158  symgcom  33159  pmtrcnel2  33166  tocyc01  33194  cycpm2tr  33195  cycpmconjv  33218  cycpmconjslem1  33230  cycpmconjslem2  33231  cycpmconjs  33232  cyc3conja  33233  1arithidomlem2  33611  mplvrpmga  33704  mplvrpmrhm  33706  reprpmtf1o  34786  hgt750lemg  34814  subfacp1lem5  35382  mrsubffval  35705  mrsubfval  35706  mrsubrn  35711  elmrsubrn  35718  upixp  38064  ltrncoidN  40588  trlcoat  41183  trlcone  41188  cdlemg47a  41194  cdlemg47  41196  ltrnco4  41199  tendovalco  41225  tendoplcbv  41235  tendopl  41236  tendoplass  41243  tendo0pl  41251  tendoipl  41257  cdlemk45  41407  cdlemk53b  41416  cdlemk55a  41419  erngdvlem3  41450  erngdvlem3-rN  41458  tendocnv  41481  dvhvaddcbv  41549  dvhvaddval  41550  dvhvaddass  41557  dicvscacl  41651  cdlemn8  41664  dihordlem7b  41675  dihopelvalcpre  41708  aks6d1c6lem5  42630  relexp2  44122  relexpxpnnidm  44148  relexpiidm  44149  relexpmulnn  44154  relexpaddss  44163  trclfvcom  44168  trclfvdecomr  44173  frege131d  44209  dssmap2d  44467  fundcmpsurbijinjpreimafv  47879  gricushgr  48405  prcof21a  49878