Theorem coeq1d 5839

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∘ ccom 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-br 5104  df-opab 5168  df-co 5660

This theorem is used by:  coeq12d  5842  fcof1oinvd  7299  domss2  9148  mapen  9153  mapfien  9393  hashfacen  14592  relexpsucnnr  15171  relexpsucnnl  15176  relexpsucr  15178  relexpsucrd  15179  relexpaddnn  15197  imasval  17676  cofuass  18057  cofulid  18058  setcinv  18258  catcisolem  18278  catciso  18279  yonedalem3b  18446  gsumvalx  18858  frmdup3lem  19055  symggrplem  19073  f1omvdco2  19655  symggen  19677  psgnunilem1  19700  gsumval3  20114  gsumzf1o  20119  znval  21834  znle2  21852  psrass1lem  22234  coe1add  22576  evls1fval  22630  evl1sca  22645  evl1var  22647  evls1var  22649  pf1mpf  22663  pf1ind  22666  tcphds  25545  dvnfval  26235  hocsubdir  32380  fcoinver  33191  fcobij  33305  cocnvf1o  33314  ccatws1f1olast  33508  symgfcoeu  33636  symgcom  33637  pmtrcnel2  33644  tocyc01  33672  cycpm2tr  33673  cycpmconjv  33696  cycpmconjslem1  33708  cycpmconjslem2  33709  cycpmconjs  33710  cyc3conja  33711  1arithidomlem2  34061  mplvrpmga  34170  mplvrpmrhm  34172  reprpmtf1o  35248  hgt750lemg  35276  subfacp1lem5  35928  mrsubffval  36251  mrsubfval  36252  mrsubrn  36257  elmrsubrn  36264  upixp  38643  ltrncoidN  41165  trlcoat  41760  trlcone  41765  cdlemg47a  41771  cdlemg47  41773  ltrnco4  41776  tendovalco  41802  tendoplcbv  41812  tendopl  41813  tendoplass  41820  tendo0pl  41828  tendoipl  41834  cdlemk45  41984  cdlemk53b  41993  cdlemk55a  41996  erngdvlem3  42027  erngdvlem3-rN  42035  tendocnv  42058  dvhvaddcbv  42126  dvhvaddval  42127  dvhvaddass  42134  dicvscacl  42228  cdlemn8  42241  dihordlem7b  42252  dihopelvalcpre  42285  aks6d1c6lem5  43207  relexp2  44662  relexpxpnnidm  44688  relexpiidm  44689  relexpmulnn  44694  relexpaddss  44703  trclfvcom  44708  trclfvdecomr  44713  frege131d  44749  dssmap2d  45007  fundcmpsurbijinjpreimafv  48458  gricushgr  48984  prcof21a  50468