Theorem coeq1 5864

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ⊆ wss 3947   ∘ ccom 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ss 3964  df-br 5154  df-opab 5216  df-co 5691

This theorem is referenced by:  coeq1i  5866  coeq1d  5868  coi2  6274  funcoeqres  6874  wrecseq123  8329  ereq1  8741  domssex2  9175  wemapwe  9740  dfttrcl2  9767  updjud  9977  seqf1olem2  14062  seqf1o  14063  relexpsucnnl  15035  isps  18593  pwsco1mhm  18822  frmdup3  18857  efmndov  18871  symggrplem  18874  smndex1mndlem  18899  smndex1mnd  18900  pmtr3ncom  19473  psgnunilem1  19491  frgpup3  19776  gsumval3  19905  rngcinv  20615  ringcinv  20649  frgpcyg  21571  frlmup4  21799  evlseu  22098  evlsval2  22102  selvval  22130  evls1val  22311  evls1sca  22314  evl1val  22320  mpfpf1  22342  pf1mpf  22343  pf1ind  22346  xkococnlem  23654  xkococn  23655  cnmpt1k  23677  cnmptkk  23678  xkofvcn  23679  qtopeu  23711  qtophmeo  23812  utop2nei  24246  cncombf  25678  dgrcolem2  26302  dgrco  26303  motplusg  28469  hocsubdir  31718  hoddi  31923  opsqrlem1  32073  1arithidom  33412  smatfval  33610  msubco  35359  coideq  37944  trljco  40439  tgrpov  40447  tendovalco  40464  erngmul  40505  erngmul-rN  40513  cdlemksv  40543  cdlemkuu  40594  cdlemk41  40619  cdleml5N  40679  cdleml9  40683  dvamulr  40711  dvavadd  40714  dvhmulr  40785  dvhvscacbv  40797  dvhvscaval  40798  dih1dimatlem0  41027  dihjatcclem4  41120  evlsval3  42031  diophrw  42416  eldioph2  42419  diophren  42470  mendmulr  42849  fundcmpsurinjpreimafv  46980  rngcinvALTV  47653  ringcinvALTV  47687  itcoval  48049