Theorem coeq1 5837

Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)

Assertion

Ref	Expression
coeq1	⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Proof of Theorem coeq1

Step	Hyp	Ref	Expression
1		coss1 5835	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶))
2		coss1 5835	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))
3	1, 2	anim12i 625	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)))
4		eqss 3946	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3946	. 2 ⊢ ((𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) ↔ ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)))
6	3, 4, 5	3imtr4i 295	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3899   ∘ ccom 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-br 5104  df-opab 5168  df-co 5664

This theorem is used by:  coeq1i  5839  coeq1d  5841  coi2  6260  funcoeqres  6850  wrecseq123  8313  ereq1  8705  domssex2  9136  wemapwe  9677  dfttrcl2  9704  updjud  9940  seqf1olem2  14107  seqf1o  14108  relexpsucnnl  15104  isps  18657  pwsco1mhm  18942  frmdup3  18977  efmndov  18991  symggrplem  18994  smndex1mndlem  19022  smndex1mnd  19023  pmtr3ncom  19603  psgnunilem1  19621  frgpup3  19906  gsumval3  20035  rngcinv  20800  ringcinv  20834  frgpcyg  21787  frlmup4  22015  evlseu  22300  evlsval2  22304  evlsval3  22306  selvval  22337  evls1val  22546  evls1sca  22549  evl1val  22555  mpfpf1  22577  pf1mpf  22578  pf1ind  22581  xkococnlem  23886  xkococn  23887  cnmpt1k  23909  cnmptkk  23910  xkofvcn  23911  qtopeu  23943  qtophmeo  24044  utop2nei  24477  cncombf  25887  dgrcolem2  26501  dgrco  26502  motplusg  28885  hocsubdir  32267  hoddi  32472  opsqrlem1  32622  1arithidom  33948  mplvrpmga  34056  mplvrpmrhm  34058  issply  34072  smatfval  34306  msubco  36111  coideq  38997  trljco  41614  tgrpov  41622  tendovalco  41639  erngmul  41680  erngmul-rN  41688  cdlemksv  41718  cdlemkuu  41769  cdlemk41  41794  cdleml5N  41854  cdleml9  41858  dvamulr  41886  dvavadd  41889  dvhmulr  41960  dvhvscacbv  41972  dvhvscaval  41973  dih1dimatlem0  42202  dihjatcclem4  42295  diophrw  43605  eldioph2  43608  diophren  43655  mendmulr  44026  fundcmpsurinjpreimafv  48309  rngcinvALTV  49192  ringcinvALTV  49226  itcoval  49592  setc1ocofval  50421