Theorem coeq2d 5014

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 5010	. 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 1438   o. ccom 4855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-in 3444  df-ss 3451  df-br 4422  df-opab 4481  df-co 4860

This theorem is referenced by:  coeq12d  5016  relcoi1OLD  5382  f1ococnv1  5857  funcoeqres  5859  fcof1oinvd  6204  foeqcnvco  6211  fparlem3  6907  fparlem4  6908  mapen  7740  mapfien  7925  wemapwe  8205  hashfacen  12616  s1co  12926  relexpsucnnl  13089  relexpsucl  13090  relexpcnv  13092  relexpaddnn  13108  relexpaddg  13110  prdsval  15346  isofval  15655  cofuass  15787  cofurid  15789  fucid  15869  setcinv  15978  catcisolem  15994  curf2ndf  16125  pwsco2mhm  16611  symggrp  17034  f1omvdco2  17082  psgnunilem1  17127  efginvrel2  17370  efginvrel1  17371  vrgpinv  17412  frgpuplem  17415  gsumval3  17534  gsumzf1o  17539  psrass1lem  18594  mpfrcl  18734  evlsval  18735  evls1fval  18901  evl1fval  18909  pf1mpf  18933  pf1ind  18936  ofco2  19468  qtophmeo  20824  ustssco  21221  utop2nei  21257  neipcfilu  21303  tngds  21648  elovolmr  22421  ovoliunlem3  22449  uniioombllem2  22532  uniioombllem2OLD  22533  hoddi  27635  fcoinver  28210  fcobij  28310  symgfcoeu  28610  smatfval  28623  eulerpartlemgv  29208  eulerpartlemn  29216  eulerpart  29217  sseqval  29223  erdsze2lem2  29929  cvmliftlem10  30019  mrsubval  30149  dfpo2  30396  ftc1anclem8  31944  cocnv  31972  ltrncoidN  33618  trlcoabs2N  34214  cdlemg47a  34226  cdlemg46  34227  cdlemg47  34228  ltrnco4  34231  tendovalco  34257  tendoplcbv  34267  tendopl  34268  tendoplass  34275  cdlemi2  34311  cdlemk2  34324  cdlemk4  34326  cdlemk8  34330  cdlemkuu  34387  cdlemk53  34449  cdlemk54  34450  cdlemk55a  34451  erngdvlem3  34482  erngdvlem3-rN  34490  tendocnv  34514  tendospcanN  34516  dvhvaddcbv  34582  dvhvaddval  34583  dvhvaddass  34590  dvhvscacbv  34591  dvhvscaval  34592  dvhopvsca  34595  dvhlveclem  34601  dvhopspN  34608  diblss  34663  cdlemn8  34697  dihopelvalcpre  34741  dihmeetlem1N  34783  dihglblem5apreN  34784  dih1dimatlem0  34821  dihjatcclem4  34914  diophrw  35526  eldioph2  35529  relexpaddss  36176  trclfvcom  36181  frege131d  36222  hoicvrrex  38159  ovnlecvr  38161  ovncvrrp  38167  ovn0lem  38168  ovnsubaddlem1  38173  ovnsubadd  38175  pfxco  38697