Theorem coeq1d 5012

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 5008	. 2 |- ( A = B -> ( A o. C ) = ( B o. C ) )
3	1, 2	syl 17	1 |- ( ph -> ( A o. C ) = ( B o. C ) )

Syntax hints:   -> wi 4   = wceq 1437   o. ccom 4854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-in 3443  df-ss 3450  df-br 4421  df-opab 4480  df-co 4859

This theorem is referenced by:  coeq12d  5015  fcof1oinvd  6203  domss2  7734  mapen  7739  mapfien  7924  hashfacen  12615  relexpsucnnr  13077  relexpsucr  13081  relexpsucnnl  13084  relexpaddnn  13103  imasval  15399  imasvalOLD  15400  cofuass  15782  cofulid  15783  setcinv  15973  catcisolem  15989  catciso  15990  yonedalem3b  16152  gsumvalx  16501  frmdup3lem  16638  symggrp  17029  f1omvdco2  17077  symggen  17099  psgnunilem1  17122  gsumval3  17529  gsumzf1o  17534  psrass1lem  18589  coe1add  18845  evls1fval  18896  evl1sca  18910  evl1var  18912  evls1var  18914  pf1mpf  18928  pf1ind  18931  znval  19093  znle2  19111  tchds  22192  dvnfval  22863  hocsubdir  27424  fcoinver  28204  fcobij  28304  symgfcoeu  28604  subfacp1lem5  29903  mrsubffval  30141  mrsubfval  30142  mrsubrn  30147  elmrsubrn  30154  upixp  31970  ltrncoidN  33612  trlcoat  34209  trlcone  34214  cdlemg47a  34220  cdlemg47  34222  ltrnco4  34225  tendovalco  34251  tendoplcbv  34261  tendopl  34262  tendoplass  34269  tendo0pl  34277  tendoipl  34283  cdlemk45  34433  cdlemk53b  34442  cdlemk55a  34445  erngdvlem3  34476  erngdvlem3-rN  34484  tendocnv  34508  dvhvaddcbv  34576  dvhvaddval  34577  dvhvaddass  34584  dicvscacl  34678  cdlemn8  34691  dihordlem7b  34702  dihopelvalcpre  34735  relexp2  36129  relexpxpnnidm  36155  relexpiidm  36156  relexpmulnn  36161  relexpaddss  36170  trclfvcom  36175  trclfvdecomr  36180  frege131d  36216