Theorem coeq1 5829

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ⊆ wss 3904   ∘ ccom 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921  df-br 5101  df-opab 5163  df-co 5656

This theorem is referenced by:  coeq1i  5831  coeq1d  5833  coi2  6251  funcoeqres  6838  wrecseq123  8294  ereq1  8686  domssex2  9109  wemapwe  9652  dfttrcl2  9679  updjud  9892  seqf1olem2  14055  seqf1o  14056  relexpsucnnl  15043  isps  18600  pwsco1mhm  18866  frmdup3  18901  efmndov  18915  symggrplem  18918  smndex1mndlem  18946  smndex1mnd  18947  pmtr3ncom  19515  psgnunilem1  19533  frgpup3  19818  gsumval3  19947  rngcinv  20687  ringcinv  20721  frgpcyg  21625  frlmup4  21853  evlseu  22136  evlsval2  22140  evlsval3  22142  selvval  22173  evls1val  22383  evls1sca  22386  evl1val  22392  mpfpf1  22414  pf1mpf  22415  pf1ind  22418  xkococnlem  23719  xkococn  23720  cnmpt1k  23742  cnmptkk  23743  xkofvcn  23744  qtopeu  23776  qtophmeo  23877  utop2nei  24310  cncombf  25720  dgrcolem2  26334  dgrco  26335  motplusg  28711  hocsubdir  31988  hoddi  32193  opsqrlem1  32343  1arithidom  33733  mplvrpmga  33842  mplvrpmrhm  33844  issply  33858  smatfval  34092  msubco  35881  coideq  38747  trljco  41364  tgrpov  41372  tendovalco  41389  erngmul  41430  erngmul-rN  41438  cdlemksv  41468  cdlemkuu  41519  cdlemk41  41544  cdleml5N  41604  cdleml9  41608  dvamulr  41636  dvavadd  41639  dvhmulr  41710  dvhvscacbv  41722  dvhvscaval  41723  dih1dimatlem0  41952  dihjatcclem4  42045  diophrw  43340  eldioph2  43343  diophren  43390  mendmulr  43761  fundcmpsurinjpreimafv  48014  rngcinvALTV  48898  ringcinvALTV  48932  itcoval  49283  setc1ocofval  50115