Theorem coeq1 5835

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 5833	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶))
2		coss1 5833	. . 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 5655

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-br 5104  df-opab 5168  df-co 5660

This theorem is used by:  coeq1i  5837  coeq1d  5839  coi2  6265  funcoeqres  6856  wrecseq123  8331  ereq1  8725  domssex2  9156  wemapwe  9698  dfttrcl2  9725  updjud  10015  seqf1olem2  14185  seqf1o  14186  relexpsucnnl  15183  isps  18742  pwsco1mhm  19028  frmdup3  19063  efmndov  19077  symggrplem  19080  smndex1mndlem  19108  smndex1mnd  19109  pmtr3ncom  19689  psgnunilem1  19707  frgpup3  19992  gsumval3  20121  rngcinv  20889  ringcinv  20923  frgpcyg  21879  frlmup4  22107  evlseu  22392  evlsval2  22396  evlsval3  22398  selvval  22429  evls1val  22638  evls1sca  22641  evl1val  22647  mpfpf1  22669  pf1mpf  22670  pf1ind  22673  xkococnlem  23978  xkococn  23979  cnmpt1k  24001  cnmptkk  24002  xkofvcn  24003  qtopeu  24035  qtophmeo  24136  utop2nei  24569  cncombf  25979  dgrcolem2  26593  dgrco  26594  motplusg  29005  hocsubdir  32387  hoddi  32592  opsqrlem1  32742  1arithidom  34069  mplvrpmga  34177  mplvrpmrhm  34179  issply  34193  smatfval  34427  msubco  36296  coideq  39180  trljco  41797  tgrpov  41805  tendovalco  41822  erngmul  41863  erngmul-rN  41871  cdlemksv  41901  cdlemkuu  41952  cdlemk41  41977  cdleml5N  42037  cdleml9  42041  dvamulr  42069  dvavadd  42072  dvhmulr  42143  dvhvscacbv  42155  dvhvscaval  42156  dih1dimatlem0  42385  dihjatcclem4  42478  diophrw  43769  eldioph2  43772  diophren  43819  mendmulr  44185  fundcmpsurinjpreimafv  48489  rngcinvALTV  49372  ringcinvALTV  49406  itcoval  49772  setc1ocofval  50601