Theorem coeq2d 5015

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

Hypothesis

Ref	Expression
coeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
coeq2d	|- ( ph -> ( C o. A ) = ( C o. B ) )

Proof of Theorem coeq2d

Step	Hyp	Ref	Expression
1		coeq1d.1	. 2 |- ( ph -> A = B )
2		coeq2 5011	. 2 |- ( A = B -> ( C o. A ) = ( C o. B ) )
3	1, 2	syl 17	1 |- ( ph -> ( C o. A ) = ( C o. B ) )

Syntax hints:   -> wi 4   = wceq 1454   o. ccom 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-in 3422  df-ss 3429  df-br 4416  df-opab 4475  df-co 4861

This theorem is referenced by:  coeq12d  5017  relcoi1OLD  5383  f1ococnv1  5864  funcoeqres  5866  fcof1oinvd  6215  foeqcnvco  6222  fparlem3  6924  fparlem4  6925  mapen  7761  mapfien  7946  wemapwe  8227  hashfacen  12649  s1co  12966  relexpsucnnl  13143  relexpsucl  13144  relexpcnv  13146  relexpaddnn  13162  relexpaddg  13164  prdsval  15401  isofval  15710  cofuass  15842  cofurid  15844  fucid  15924  setcinv  16033  catcisolem  16049  curf2ndf  16180  pwsco2mhm  16666  symggrp  17089  f1omvdco2  17137  psgnunilem1  17182  efginvrel2  17425  efginvrel1  17426  vrgpinv  17467  frgpuplem  17470  gsumval3  17589  gsumzf1o  17594  psrass1lem  18649  mpfrcl  18789  evlsval  18790  evls1fval  18956  evl1fval  18964  pf1mpf  18988  pf1ind  18991  ofco2  19524  qtophmeo  20880  ustssco  21277  utop2nei  21313  neipcfilu  21359  tngds  21704  elovolmr  22477  ovoliunlem3  22505  uniioombllem2  22588  uniioombllem2OLD  22589  hoddi  27691  fcoinver  28262  fcobij  28358  symgfcoeu  28656  smatfval  28669  eulerpartlemgv  29254  eulerpartlemn  29262  eulerpart  29263  sseqval  29269  erdsze2lem2  29975  cvmliftlem10  30065  mrsubval  30195  dfpo2  30443  ftc1anclem8  32068  cocnv  32096  ltrncoidN  33737  trlcoabs2N  34333  cdlemg47a  34345  cdlemg46  34346  cdlemg47  34347  ltrnco4  34350  tendovalco  34376  tendoplcbv  34386  tendopl  34387  tendoplass  34394  cdlemi2  34430  cdlemk2  34443  cdlemk4  34445  cdlemk8  34449  cdlemkuu  34506  cdlemk53  34568  cdlemk54  34569  cdlemk55a  34570  erngdvlem3  34601  erngdvlem3-rN  34609  tendocnv  34633  tendospcanN  34635  dvhvaddcbv  34701  dvhvaddval  34702  dvhvaddass  34709  dvhvscacbv  34710  dvhvscaval  34711  dvhopvsca  34714  dvhlveclem  34720  dvhopspN  34727  diblss  34782  cdlemn8  34816  dihopelvalcpre  34860  dihmeetlem1N  34902  dihglblem5apreN  34903  dih1dimatlem0  34940  dihjatcclem4  35033  diophrw  35645  eldioph2  35648  relexpaddss  36354  trclfvcom  36359  frege131d  36400  hoicvrrex  38415  ovnlecvr  38417  ovncvrrp  38423  ovn0lem  38424  ovnsubaddlem1  38429  ovnsubadd  38431  ovnhoilem1  38460  ovnhoi  38462  ovnlecvr2  38469  ovncvr2  38470  hspmbl  38488  pfxco  39018