Theorem coeq1 5845

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923  df-br 5112  df-opab 5176  df-co 5672

This theorem is used by:  coeq1i  5847  coeq1d  5849  coi2  6267  funcoeqres  6856  wrecseq123  8316  ereq1  8708  domssex2  9132  wemapwe  9673  dfttrcl2  9700  updjud  9936  seqf1olem2  14098  seqf1o  14099  relexpsucnnl  15093  isps  18648  pwsco1mhm  18930  frmdup3  18965  efmndov  18979  symggrplem  18982  smndex1mndlem  19010  smndex1mnd  19011  pmtr3ncom  19591  psgnunilem1  19609  frgpup3  19894  gsumval3  20023  rngcinv  20788  ringcinv  20822  frgpcyg  21775  frlmup4  22003  evlseu  22286  evlsval2  22290  evlsval3  22292  selvval  22323  evls1val  22532  evls1sca  22535  evl1val  22541  mpfpf1  22563  pf1mpf  22564  pf1ind  22567  xkococnlem  23869  xkococn  23870  cnmpt1k  23892  cnmptkk  23893  xkofvcn  23894  qtopeu  23926  qtophmeo  24027  utop2nei  24460  cncombf  25870  dgrcolem2  26484  dgrco  26485  motplusg  28864  hocsubdir  32210  hoddi  32415  opsqrlem1  32565  1arithidom  33893  mplvrpmga  34001  mplvrpmrhm  34003  issply  34017  smatfval  34251  msubco  36062  coideq  38957  trljco  41574  tgrpov  41582  tendovalco  41599  erngmul  41640  erngmul-rN  41648  cdlemksv  41678  cdlemkuu  41729  cdlemk41  41754  cdleml5N  41814  cdleml9  41818  dvamulr  41846  dvavadd  41849  dvhmulr  41920  dvhvscacbv  41932  dvhvscaval  41933  dih1dimatlem0  42162  dihjatcclem4  42255  diophrw  43550  eldioph2  43553  diophren  43600  mendmulr  43971  fundcmpsurinjpreimafv  48217  rngcinvALTV  49100  ringcinvALTV  49134  itcoval  49500  setc1ocofval  50331