Theorem coeq1 5858

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 5856	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶))
2		coss1 5856	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))
3	1, 2	anim12i 614	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)))
4		eqss 3998	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3998	. 2 ⊢ ((𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) ↔ ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ⊆ wss 3949   ∘ ccom 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-co 5686

This theorem is referenced by:  coeq1i  5860  coeq1d  5862  coi2  6263  funcoeqres  6865  wrecseq123  8299  ereq1  8710  domssex2  9137  wemapwe  9692  dfttrcl2  9719  updjud  9929  seqf1olem2  14008  seqf1o  14009  relexpsucnnl  14977  isps  18521  pwsco1mhm  18713  frmdup3  18748  efmndov  18762  symggrplem  18765  smndex1mndlem  18790  smndex1mnd  18791  pmtr3ncom  19343  psgnunilem1  19361  frgpup3  19646  gsumval3  19775  frgpcyg  21129  frlmup4  21356  evlseu  21646  evlsval2  21650  selvval  21681  evls1val  21839  evls1sca  21842  evl1val  21848  mpfpf1  21870  pf1mpf  21871  pf1ind  21874  xkococnlem  23163  xkococn  23164  cnmpt1k  23186  cnmptkk  23187  xkofvcn  23188  qtopeu  23220  qtophmeo  23321  utop2nei  23755  cncombf  25175  dgrcolem2  25788  dgrco  25789  motplusg  27793  hocsubdir  31038  hoddi  31243  opsqrlem1  31393  smatfval  32775  msubco  34522  coideq  37113  trljco  39611  tgrpov  39619  tendovalco  39636  erngmul  39677  erngmul-rN  39685  cdlemksv  39715  cdlemkuu  39766  cdlemk41  39791  cdleml5N  39851  cdleml9  39855  dvamulr  39883  dvavadd  39886  dvhmulr  39957  dvhvscacbv  39969  dvhvscaval  39970  dih1dimatlem0  40199  dihjatcclem4  40292  evlsval3  41131  diophrw  41497  eldioph2  41500  diophren  41551  mendmulr  41930  fundcmpsurinjpreimafv  46076  rngcinv  46879  rngcinvALTV  46891  ringcinv  46930  ringcinvALTV  46954  itcoval  47347