Theorem coeq1d 5841

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 5837	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Syntax hints:   → wi 4   = wceq 1540   ∘ ccom 5658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-br 5120  df-opab 5182  df-co 5663

This theorem is referenced by:  coeq12d  5844  fcof1oinvd  7285  domss2  9148  mapen  9153  mapfien  9418  hashfacen  14470  relexpsucnnr  15042  relexpsucnnl  15047  relexpsucr  15049  relexpsucrd  15050  relexpaddnn  15068  imasval  17523  cofuass  17900  cofulid  17901  setcinv  18101  catcisolem  18121  catciso  18122  yonedalem3b  18289  gsumvalx  18652  frmdup3lem  18842  symggrplem  18860  f1omvdco2  19427  symggen  19449  psgnunilem1  19472  gsumval3  19886  gsumzf1o  19891  znval  21494  znle2  21512  psrass1lem  21890  coe1add  22199  evls1fval  22255  evl1sca  22270  evl1var  22272  evls1var  22274  pf1mpf  22288  pf1ind  22291  tcphds  25181  dvnfval  25874  hocsubdir  31712  fcoinver  32531  fcobij  32645  ccatws1f1olast  32874  symgfcoeu  33039  symgcom  33040  pmtrcnel2  33047  tocyc01  33075  cycpm2tr  33076  cycpmconjv  33099  cycpmconjslem1  33111  cycpmconjslem2  33112  cycpmconjs  33113  cyc3conja  33114  1arithidomlem2  33497  reprpmtf1o  34604  hgt750lemg  34632  subfacp1lem5  35152  mrsubffval  35475  mrsubfval  35476  mrsubrn  35481  elmrsubrn  35488  upixp  37699  ltrncoidN  40093  trlcoat  40688  trlcone  40693  cdlemg47a  40699  cdlemg47  40701  ltrnco4  40704  tendovalco  40730  tendoplcbv  40740  tendopl  40741  tendoplass  40748  tendo0pl  40756  tendoipl  40762  cdlemk45  40912  cdlemk53b  40921  cdlemk55a  40924  erngdvlem3  40955  erngdvlem3-rN  40963  tendocnv  40986  dvhvaddcbv  41054  dvhvaddval  41055  dvhvaddass  41062  dicvscacl  41156  cdlemn8  41169  dihordlem7b  41180  dihopelvalcpre  41213  aks6d1c6lem5  42136  relexp2  43648  relexpxpnnidm  43674  relexpiidm  43675  relexpmulnn  43680  relexpaddss  43689  trclfvcom  43694  trclfvdecomr  43699  frege131d  43735  dssmap2d  43993  fundcmpsurbijinjpreimafv  47369  gricushgr  47878  prcof21a  49249