Theorem coeq1 5843

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ⊆ wss 3905   ∘ ccom 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-br 5110  df-opab 5174  df-co 5670

This theorem is referenced by:  coeq1i  5845  coeq1d  5847  coi2  6265  funcoeqres  6852  wrecseq123  8306  ereq1  8698  domssex2  9121  wemapwe  9662  dfttrcl2  9689  updjud  9916  seqf1olem2  14074  seqf1o  14075  relexpsucnnl  15063  isps  18619  pwsco1mhm  18886  frmdup3  18921  efmndov  18935  symggrplem  18938  smndex1mndlem  18966  smndex1mnd  18967  pmtr3ncom  19540  psgnunilem1  19558  frgpup3  19843  gsumval3  19972  rngcinv  20736  ringcinv  20770  frgpcyg  21723  frlmup4  21951  evlseu  22234  evlsval2  22238  evlsval3  22240  selvval  22271  evls1val  22480  evls1sca  22483  evl1val  22489  mpfpf1  22511  pf1mpf  22512  pf1ind  22515  xkococnlem  23816  xkococn  23817  cnmpt1k  23839  cnmptkk  23840  xkofvcn  23841  qtopeu  23873  qtophmeo  23974  utop2nei  24407  cncombf  25817  dgrcolem2  26431  dgrco  26432  motplusg  28811  hocsubdir  32137  hoddi  32342  opsqrlem1  32492  1arithidom  33827  mplvrpmga  33935  mplvrpmrhm  33937  issply  33951  smatfval  34185  msubco  36023  coideq  38917  trljco  41534  tgrpov  41542  tendovalco  41559  erngmul  41600  erngmul-rN  41608  cdlemksv  41638  cdlemkuu  41689  cdlemk41  41714  cdleml5N  41774  cdleml9  41778  dvamulr  41806  dvavadd  41809  dvhmulr  41880  dvhvscacbv  41892  dvhvscaval  41893  dih1dimatlem0  42122  dihjatcclem4  42215  diophrw  43510  eldioph2  43513  diophren  43560  mendmulr  43931  fundcmpsurinjpreimafv  48177  rngcinvALTV  49061  ringcinvALTV  49095  itcoval  49461  setc1ocofval  50292