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 1569   ∘ ccom 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3897  df-br 5103  df-opab 5167  df-co 5659

This theorem is used by:  coeq12d  5842  fcof1oinvd  7303  domss2  9160  mapen  9165  mapfien  9405  hashfacen  14604  relexpsucnnr  15185  relexpsucnnl  15190  relexpsucr  15192  relexpsucrd  15193  relexpaddnn  15211  imasval  17690  cofuass  18071  cofulid  18072  setcinv  18272  catcisolem  18292  catciso  18293  yonedalem3b  18460  gsumvalx  18872  frmdup3lem  19069  symggrplem  19087  f1omvdco2  19669  symggen  19691  psgnunilem1  19714  gsumval3  20128  gsumzf1o  20133  znval  21848  znle2  21866  psrass1lem  22248  coe1add  22590  evls1fval  22644  evl1sca  22659  evl1var  22661  evls1var  22663  pf1mpf  22677  pf1ind  22680  tcphds  25559  dvnfval  26249  hocsubdir  32394  fcoinver  33247  fcobij  33360  cocnvf1o  33369  ccatws1f1olast  33563  symgfcoeu  33691  symgcom  33692  pmtrcnel2  33699  tocyc01  33727  cycpm2tr  33728  cycpmconjv  33751  cycpmconjslem1  33763  cycpmconjslem2  33764  cycpmconjs  33765  cyc3conja  33766  1arithidomlem2  34116  mplvrpmga  34225  mplvrpmrhm  34227  reprpmtf1o  35303  hgt750lemg  35331  subfacp1lem5  36037  mrsubffval  36360  mrsubfval  36361  mrsubrn  36366  elmrsubrn  36373  upixp  38770  ltrncoidN  41292  trlcoat  41887  trlcone  41892  cdlemg47a  41898  cdlemg47  41900  ltrnco4  41903  tendovalco  41929  tendoplcbv  41939  tendopl  41940  tendoplass  41947  tendo0pl  41955  tendoipl  41961  cdlemk45  42111  cdlemk53b  42120  cdlemk55a  42123  erngdvlem3  42154  erngdvlem3-rN  42162  tendocnv  42185  dvhvaddcbv  42253  dvhvaddval  42254  dvhvaddass  42261  dicvscacl  42355  cdlemn8  42368  dihordlem7b  42379  dihopelvalcpre  42412  aks6d1c6lem5  43334  relexp2  44784  relexpxpnnidm  44810  relexpiidm  44811  relexpmulnn  44816  relexpaddss  44825  trclfvcom  44830  trclfvdecomr  44835  frege131d  44871  dssmap2d  45129  fundcmpsurbijinjpreimafv  48596  gricushgr  49122  cofu1stfix  50319  prcof21a  50633