Theorem coeq1 5839

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ⊆ wss 3899   ∘ ccom 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3900  df-br 5106  df-opab 5170  df-co 5663

This theorem is used by:  coeq1i  5841  coeq1d  5843  coi2  6271  funcoeqres  6864  wrecseq123  8342  ereq1  8736  domssex2  9167  wemapwe  9708  dfttrcl2  9735  updjud  10025  seqf1olem2  14195  seqf1o  14196  relexpsucnnl  15195  isps  18754  pwsco1mhm  19040  frmdup3  19075  efmndov  19089  symggrplem  19092  smndex1mndlem  19120  smndex1mnd  19121  pmtr3ncom  19701  psgnunilem1  19719  frgpup3  20004  gsumval3  20133  rngcinv  20901  ringcinv  20935  frgpcyg  21891  frlmup4  22119  evlseu  22404  evlsval2  22408  evlsval3  22410  selvval  22441  evls1val  22650  evls1sca  22653  evl1val  22659  mpfpf1  22681  pf1mpf  22682  pf1ind  22685  xkococnlem  23990  xkococn  23991  cnmpt1k  24013  cnmptkk  24014  xkofvcn  24015  qtopeu  24047  qtophmeo  24148  utop2nei  24581  cncombf  25991  dgrcolem2  26605  dgrco  26606  motplusg  29017  hocsubdir  32399  hoddi  32604  opsqrlem1  32754  1arithidom  34122  mplvrpmga  34230  mplvrpmrhm  34232  issply  34246  smatfval  34480  msubco  36417  coideq  39320  trljco  41937  tgrpov  41945  tendovalco  41962  erngmul  42003  erngmul-rN  42011  cdlemksv  42041  cdlemkuu  42092  cdlemk41  42117  cdleml5N  42177  cdleml9  42181  dvamulr  42209  dvavadd  42212  dvhmulr  42283  dvhvscacbv  42295  dvhvscaval  42296  dih1dimatlem0  42525  dihjatcclem4  42618  diophrw  43910  eldioph2  43913  diophren  43960  mendmulr  44326  fundcmpsurinjpreimafv  48629  rngcinvALTV  49512  ringcinvALTV  49546  itcoval  49912  setc1ocofval  50768