Theorem coeq1 5814

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3903   ∘ ccom 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-br 5101  df-opab 5163  df-co 5641

This theorem is referenced by:  coeq1i  5816  coeq1d  5818  coi2  6230  funcoeqres  6813  wrecseq123  8265  ereq1  8653  domssex2  9077  wemapwe  9618  dfttrcl2  9645  updjud  9858  seqf1olem2  13977  seqf1o  13978  relexpsucnnl  14965  isps  18503  pwsco1mhm  18769  frmdup3  18804  efmndov  18818  symggrplem  18821  smndex1mndlem  18846  smndex1mnd  18847  pmtr3ncom  19416  psgnunilem1  19434  frgpup3  19719  gsumval3  19848  rngcinv  20582  ringcinv  20616  frgpcyg  21540  frlmup4  21768  evlseu  22050  evlsval2  22054  evlsval3  22056  selvval  22090  evls1val  22276  evls1sca  22279  evl1val  22285  mpfpf1  22307  pf1mpf  22308  pf1ind  22311  xkococnlem  23615  xkococn  23616  cnmpt1k  23638  cnmptkk  23639  xkofvcn  23640  qtopeu  23672  qtophmeo  23773  utop2nei  24206  cncombf  25627  dgrcolem2  26248  dgrco  26249  motplusg  28626  hocsubdir  31873  hoddi  32078  opsqrlem1  32228  1arithidom  33630  mplvrpmga  33722  mplvrpmrhm  33724  issply  33738  smatfval  33973  msubco  35747  coideq  38499  trljco  41116  tgrpov  41124  tendovalco  41141  erngmul  41182  erngmul-rN  41190  cdlemksv  41220  cdlemkuu  41271  cdlemk41  41296  cdleml5N  41356  cdleml9  41360  dvamulr  41388  dvavadd  41391  dvhmulr  41462  dvhvscacbv  41474  dvhvscaval  41475  dih1dimatlem0  41704  dihjatcclem4  41797  diophrw  43116  eldioph2  43119  diophren  43170  mendmulr  43541  fundcmpsurinjpreimafv  47768  rngcinvALTV  48636  ringcinvALTV  48670  itcoval  49021  setc1ocofval  49853