Theorem coeq2d 5811

Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)

Hypothesis

Ref	Expression
coeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
coeq2d	⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

Proof of Theorem coeq2d

Step	Hyp	Ref	Expression
1		coeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		coeq2 5807	. 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  dfpo2  6254  f1ococnv1  6803  funcoeqres  6805  fcof1oinvd  7241  foeqcnvco  7248  f1ofvswap  7254  coof  7648  fparlem3  8057  fparlem4  8058  offsplitfpar  8062  csbwrecsg  8261  mapen  9072  mapfien  9314  wemapwe  9609  hashfacen  14407  s1co  14786  pfxco  14791  relexpsucnnl  14983  relexpsucl  14984  relexpsucld  14987  relexpcnv  14988  relexpaddnn  15004  relexpaddg  15006  prdsval  17409  isofval  17715  cofuass  17847  cofurid  17849  fucid  17932  setcinv  18048  catcisolem  18068  curf2ndf  18204  pwsco2mhm  18792  symggrplem  18843  smndex1igid  18865  smndex1igidOLD  18866  f1omvdco2  19414  psgnunilem1  19459  efginvrel2  19693  efginvrel1  19694  vrgpinv  19735  frgpuplem  19738  gsumval3  19873  gsumzf1o  19878  psrass1lem  21922  mpfrcl  22073  evlsval  22074  selvval  22111  evls1fval  22294  evl1fval  22303  pf1mpf  22327  pf1ind  22330  mhmcoaddmpl  22356  rhmcomulmpl  22357  rhmmpl  22358  rhmply1vr1  22362  rhmply1vsca  22363  ofco2  22426  qtophmeo  23792  ustssco  24190  utop2nei  24225  neipcfilu  24270  tngds  24623  elovolmr  25453  ovoliunlem3  25481  uniioombllem2  25560  hoddi  32076  fcoinver  32689  fmptco1f1o  32721  fcobij  32808  cocnvf1o  32817  symgfcoeu  33158  symgcom  33159  tocycf  33193  tocyc01  33194  cycpmconjvlem  33217  cycpmconjv  33218  cycpmconjslem1  33230  cycpmconjslem2  33231  cycpmconjs  33232  cyc3conja  33233  1arithidomlem2  33611  mplvrpmga  33704  mplvrpmrhm  33706  esplyfval  33722  esplyfval0  33723  esplyfval2  33724  vieta  33739  smatfval  33955  eulerpartlemgv  34533  eulerpartlemn  34541  eulerpart  34542  sseqval  34548  reprpmtf1o  34786  erdsze2lem2  35402  cvmliftlem10  35492  mrsubval  35707  ftc1anclem8  38035  cocnv  38060  ltrncoidN  40588  trlcoabs2N  41182  cdlemg47a  41194  cdlemg46  41195  cdlemg47  41196  ltrnco4  41199  tendovalco  41225  tendoplcbv  41235  tendopl  41236  tendoplass  41243  cdlemi2  41279  cdlemk2  41292  cdlemk4  41294  cdlemk8  41298  cdlemkuu  41355  cdlemk53  41417  cdlemk54  41418  cdlemk55a  41419  erngdvlem3  41450  erngdvlem3-rN  41458  tendocnv  41481  tendospcanN  41483  dvhvaddcbv  41549  dvhvaddval  41550  dvhvaddass  41557  dvhvscacbv  41558  dvhvscaval  41559  dvhopvsca  41562  dvhlveclem  41568  dvhopspN  41575  diblss  41630  cdlemn8  41664  dihopelvalcpre  41708  dihmeetlem1N  41750  dihglblem5apreN  41751  dih1dimatlem0  41788  dihjatcclem4  41881  aks6d1c6lem5  42630  mhmcoaddpsr  43007  rhmcomulpsr  43008  rhmpsr  43009  diophrw  43205  eldioph2  43208  relexpaddss  44163  trclfvcom  44168  frege131d  44209  fsovrfovd  44454  hoicvrrex  47002  ovnlecvr  47004  ovncvrrp  47010  ovn0lem  47011  ovnsubaddlem1  47016  ovnsubadd  47018  ovnhoilem1  47047  ovnhoi  47049  ovnlecvr2  47056  ovncvr2  47057  hspmbl  47075  ovnovollem1  47102  ovnovollem3  47104  3f1oss2  47536  cosn  49321  fuco11id  49821  fucoid  49835  precofval3  49858  prcofvalg  49863  prcofval  49865