Theorem coeq1d 5153

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
coeq1d	|- ( ph -> ( A o. C ) = ( B o. C ) )

Proof of Theorem coeq1d

Step	Hyp	Ref	Expression
1		coeq1d.1	. 2 |- ( ph -> A = B )
2		coeq1 5149	. 2 |- ( A = B -> ( A o. C ) = ( B o. C ) )
3	1, 2	syl 16	1 |- ( ph -> ( A o. C ) = ( B o. C ) )

Syntax hints:   -> wi 4   = wceq 1398   o. ccom 4992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-in 3468  df-ss 3475  df-br 4440  df-opab 4498  df-co 4997

This theorem is referenced by:  coeq12d  5156  fcof1oinvd  6171  domss2  7669  mapen  7674  mapfien  7859  mapfienOLD  8129  hashfacen  12487  relexpsucnnr  12942  relexpsucr  12944  relexpsucnnl  12947  relexpaddnn  12966  imasval  15000  cofuass  15377  cofulid  15378  setcinv  15568  catcisolem  15584  catciso  15585  yonedalem3b  15747  gsumvalx  16096  frmdup3lem  16233  symggrp  16624  f1omvdco2  16672  symggen  16694  psgnunilem1  16717  gsumval3OLD  17107  gsumval3  17110  gsumzf1o  17116  gsumzf1oOLD  17119  psrass1lem  18224  coe1add  18500  evls1fval  18551  evl1sca  18565  evl1var  18567  evls1var  18569  pf1mpf  18583  pf1ind  18586  znval  18747  znle2  18765  tchds  21840  dvnfval  22491  hocsubdir  26902  fcoinver  27674  fcobij  27779  subfacp1lem5  28892  mrsubffval  29131  mrsubfval  29132  mrsubrn  29137  elmrsubrn  29144  upixp  30460  ltrncoidN  36249  trlcoat  36846  trlcone  36851  cdlemg47a  36857  cdlemg47  36859  ltrnco4  36862  tendovalco  36888  tendoplcbv  36898  tendopl  36899  tendoplass  36906  tendo0pl  36914  tendoipl  36920  cdlemk45  37070  cdlemk53b  37079  cdlemk55a  37082  erngdvlem3  37113  erngdvlem3-rN  37121  tendocnv  37145  dvhvaddcbv  37213  dvhvaddval  37214  dvhvaddass  37221  dicvscacl  37315  cdlemn8  37328  dihordlem7b  37339  dihopelvalcpre  37372  relexp2  38198  relexpaddss  38205  relexpiidm  38222  relexpxpnnidm  38225  relexpmulnn  38227