Theorem coeq1d 5864

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

Syntax hints:   → wi 4   = wceq 1533   ∘ ccom 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ss 3961  df-br 5150  df-opab 5212  df-co 5687

This theorem is referenced by:  coeq12d  5867  fcof1oinvd  7302  domss2  9161  mapen  9166  mapfien  9433  hashfacen  14449  hashfacenOLD  14450  relexpsucnnr  15008  relexpsucnnl  15013  relexpsucr  15015  relexpsucrd  15016  relexpaddnn  15034  imasval  17496  cofuass  17878  cofulid  17879  setcinv  18082  catcisolem  18102  catciso  18103  yonedalem3b  18274  gsumvalx  18639  frmdup3lem  18826  symggrplem  18844  f1omvdco2  19415  symggen  19437  psgnunilem1  19460  gsumval3  19874  gsumzf1o  19879  znval  21482  znle2  21504  psrass1lemOLD  21891  psrass1lem  21894  coe1add  22208  evls1fval  22263  evl1sca  22278  evl1var  22280  evls1var  22282  pf1mpf  22296  pf1ind  22299  tcphds  25203  dvnfval  25896  hocsubdir  31667  fcoinver  32473  fcobij  32586  ccatws1f1olast  32762  symgfcoeu  32895  symgcom  32896  pmtrcnel2  32903  tocyc01  32931  cycpm2tr  32932  cycpmconjv  32955  cycpmconjslem1  32967  cycpmconjslem2  32968  cycpmconjs  32969  cyc3conja  32970  1arithidomlem2  33348  reprpmtf1o  34389  hgt750lemg  34417  subfacp1lem5  34925  mrsubffval  35248  mrsubfval  35249  mrsubrn  35254  elmrsubrn  35261  upixp  37333  ltrncoidN  39731  trlcoat  40326  trlcone  40331  cdlemg47a  40337  cdlemg47  40339  ltrnco4  40342  tendovalco  40368  tendoplcbv  40378  tendopl  40379  tendoplass  40386  tendo0pl  40394  tendoipl  40400  cdlemk45  40550  cdlemk53b  40559  cdlemk55a  40562  erngdvlem3  40593  erngdvlem3-rN  40601  tendocnv  40624  dvhvaddcbv  40692  dvhvaddval  40693  dvhvaddass  40700  dicvscacl  40794  cdlemn8  40807  dihordlem7b  40818  dihopelvalcpre  40851  aks6d1c6lem5  41780  relexp2  43249  relexpxpnnidm  43275  relexpiidm  43276  relexpmulnn  43281  relexpaddss  43290  trclfvcom  43295  trclfvdecomr  43300  frege131d  43336  dssmap2d  43594  fundcmpsurbijinjpreimafv  46884  gricushgr  47369