Theorem coeq1 5846

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5109  df-opab 5174  df-co 5667

This theorem is used by:  coeq1i  5848  coeq1d  5850  coi2  6286  funcoeqres  6887  wrecseq123  8369  ereq1  8763  domssex2  9194  wemapwe  9735  dfttrcl2  9762  updjud  10052  seqf1olem2  14225  seqf1o  14226  relexpsucnnl  15226  isps  18792  pwsco1mhm  19078  frmdup3  19113  efmndov  19127  symggrplem  19130  smndex1mndlem  19158  smndex1mnd  19159  pmtr3ncom  19740  psgnunilem1  19758  frgpup3  20043  gsumval3  20172  rngcinv  20940  ringcinv  20974  frgpcyg  21934  frlmup4  22162  evlseu  22447  evlsval2  22451  evlsval3  22453  selvval  22484  evls1val  22693  evls1sca  22696  evl1val  22702  mpfpf1  22724  pf1mpf  22725  pf1ind  22728  xkococnlem  24033  xkococn  24034  cnmpt1k  24056  cnmptkk  24057  xkofvcn  24058  qtopeu  24090  qtophmeo  24191  utop2nei  24624  cncombf  26034  dgrcolem2  26648  dgrco  26649  motplusg  29062  hocsubdir  32444  hoddi  32649  opsqrlem1  32799  1arithidom  34173  mplvrpmga  34288  mplvrpmrhm  34290  issply  34304  smatfval  34538  msubco  36504  coideq  39446  trljco  42063  tgrpov  42071  tendovalco  42088  erngmul  42129  erngmul-rN  42137  cdlemksv  42167  cdlemkuu  42218  cdlemk41  42243  cdleml5N  42303  cdleml9  42307  dvamulr  42335  dvavadd  42338  dvhmulr  42409  dvhvscacbv  42421  dvhvscaval  42422  dih1dimatlem0  42651  dihjatcclem4  42744  diophrw  44036  eldioph2  44039  diophren  44086  mendmulr  44447  hfstructwe  46303  fundcmpsurinjpreimafv  48763  rngcinvALTV  49646  ringcinvALTV  49680  itcoval  50104  setc1ocofval  50960