Theorem coeq1d 5759

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

Hypothesis

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

Assertion

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

Proof of Theorem coeq1d

Step	Hyp	Ref	Expression
1		coeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		coeq1 5755	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Syntax hints:   → wi 4   = wceq 1539   ∘ ccom 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071  df-opab 5133  df-co 5589

This theorem is referenced by:  coeq12d  5762  fcof1oinvd  7145  domss2  8872  mapen  8877  mapfien  9097  hashfacen  14094  hashfacenOLD  14095  relexpsucnnr  14664  relexpsucnnl  14669  relexpsucr  14671  relexpsucrd  14672  relexpaddnn  14690  imasval  17139  cofuass  17520  cofulid  17521  setcinv  17721  catcisolem  17741  catciso  17742  yonedalem3b  17913  gsumvalx  18275  frmdup3lem  18420  symggrplem  18438  f1omvdco2  18971  symggen  18993  psgnunilem1  19016  gsumval3  19423  gsumzf1o  19428  znval  20651  znle2  20673  psrass1lemOLD  21053  psrass1lem  21056  coe1add  21345  evls1fval  21395  evl1sca  21410  evl1var  21412  evls1var  21414  pf1mpf  21428  pf1ind  21431  tcphds  24300  dvnfval  24991  hocsubdir  30048  fcoinver  30847  fcobij  30959  symgfcoeu  31253  symgcom  31254  pmtrcnel2  31261  tocyc01  31287  cycpm2tr  31288  cycpmconjv  31311  cycpmconjslem1  31323  cycpmconjslem2  31324  cycpmconjs  31325  cyc3conja  31326  reprpmtf1o  32506  hgt750lemg  32534  subfacp1lem5  33046  mrsubffval  33369  mrsubfval  33370  mrsubrn  33375  elmrsubrn  33382  upixp  35814  ltrncoidN  38069  trlcoat  38664  trlcone  38669  cdlemg47a  38675  cdlemg47  38677  ltrnco4  38680  tendovalco  38706  tendoplcbv  38716  tendopl  38717  tendoplass  38724  tendo0pl  38732  tendoipl  38738  cdlemk45  38888  cdlemk53b  38897  cdlemk55a  38900  erngdvlem3  38931  erngdvlem3-rN  38939  tendocnv  38962  dvhvaddcbv  39030  dvhvaddval  39031  dvhvaddass  39038  dicvscacl  39132  cdlemn8  39145  dihordlem7b  39156  dihopelvalcpre  39189  relexp2  41174  relexpxpnnidm  41200  relexpiidm  41201  relexpmulnn  41206  relexpaddss  41215  trclfvcom  41220  trclfvdecomr  41225  frege131d  41261  dssmap2d  41519  fundcmpsurbijinjpreimafv  44747  isomushgr  45166