Theorem coeq1d 5818

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

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

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 3920  df-br 5101  df-opab 5163  df-co 5641

This theorem is referenced by:  coeq12d  5821  fcof1oinvd  7249  domss2  9076  mapen  9081  mapfien  9323  hashfacen  14389  relexpsucnnr  14960  relexpsucnnl  14965  relexpsucr  14967  relexpsucrd  14968  relexpaddnn  14986  imasval  17444  cofuass  17825  cofulid  17826  setcinv  18026  catcisolem  18046  catciso  18047  yonedalem3b  18214  gsumvalx  18613  frmdup3lem  18803  symggrplem  18821  f1omvdco2  19389  symggen  19411  psgnunilem1  19434  gsumval3  19848  gsumzf1o  19853  znval  21502  znle2  21520  psrass1lem  21900  coe1add  22218  evls1fval  22275  evl1sca  22290  evl1var  22292  evls1var  22294  pf1mpf  22308  pf1ind  22311  tcphds  25199  dvnfval  25892  hocsubdir  31873  fcoinver  32691  fcobij  32810  cocnvf1o  32819  ccatws1f1olast  33045  symgfcoeu  33176  symgcom  33177  pmtrcnel2  33184  tocyc01  33212  cycpm2tr  33213  cycpmconjv  33236  cycpmconjslem1  33248  cycpmconjslem2  33249  cycpmconjs  33250  cyc3conja  33251  1arithidomlem2  33629  mplvrpmga  33722  mplvrpmrhm  33724  reprpmtf1o  34804  hgt750lemg  34832  subfacp1lem5  35400  mrsubffval  35723  mrsubfval  35724  mrsubrn  35729  elmrsubrn  35736  upixp  37980  ltrncoidN  40504  trlcoat  41099  trlcone  41104  cdlemg47a  41110  cdlemg47  41112  ltrnco4  41115  tendovalco  41141  tendoplcbv  41151  tendopl  41152  tendoplass  41159  tendo0pl  41167  tendoipl  41173  cdlemk45  41323  cdlemk53b  41332  cdlemk55a  41335  erngdvlem3  41366  erngdvlem3-rN  41374  tendocnv  41397  dvhvaddcbv  41465  dvhvaddval  41466  dvhvaddass  41473  dicvscacl  41567  cdlemn8  41580  dihordlem7b  41591  dihopelvalcpre  41624  aks6d1c6lem5  42547  relexp2  44033  relexpxpnnidm  44059  relexpiidm  44060  relexpmulnn  44065  relexpaddss  44074  trclfvcom  44079  trclfvdecomr  44084  frege131d  44120  dssmap2d  44378  fundcmpsurbijinjpreimafv  47767  gricushgr  48277  prcof21a  49750