Theorem coeq1 5800

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3903   ∘ ccom 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3920  df-br 5093  df-opab 5155  df-co 5628

This theorem is referenced by:  coeq1i  5802  coeq1d  5804  coi2  6212  funcoeqres  6795  wrecseq123  8246  ereq1  8632  domssex2  9054  wemapwe  9593  dfttrcl2  9620  updjud  9830  seqf1olem2  13949  seqf1o  13950  relexpsucnnl  14937  isps  18474  pwsco1mhm  18706  frmdup3  18741  efmndov  18755  symggrplem  18758  smndex1mndlem  18783  smndex1mnd  18784  pmtr3ncom  19354  psgnunilem1  19372  frgpup3  19657  gsumval3  19786  rngcinv  20522  ringcinv  20556  frgpcyg  21480  frlmup4  21708  evlseu  21988  evlsval2  21992  selvval  22020  evls1val  22205  evls1sca  22208  evl1val  22214  mpfpf1  22236  pf1mpf  22237  pf1ind  22240  xkococnlem  23544  xkococn  23545  cnmpt1k  23567  cnmptkk  23568  xkofvcn  23569  qtopeu  23601  qtophmeo  23702  utop2nei  24136  cncombf  25557  dgrcolem2  26178  dgrco  26179  motplusg  28487  hocsubdir  31729  hoddi  31934  opsqrlem1  32084  1arithidom  33474  mplvrpmga  33546  smatfval  33762  msubco  35508  coideq  38225  trljco  40723  tgrpov  40731  tendovalco  40748  erngmul  40789  erngmul-rN  40797  cdlemksv  40827  cdlemkuu  40878  cdlemk41  40903  cdleml5N  40963  cdleml9  40967  dvamulr  40995  dvavadd  40998  dvhmulr  41069  dvhvscacbv  41081  dvhvscaval  41082  dih1dimatlem0  41311  dihjatcclem4  41404  evlsval3  42536  diophrw  42736  eldioph2  42739  diophren  42790  mendmulr  43161  fundcmpsurinjpreimafv  47396  rngcinvALTV  48264  ringcinvALTV  48298  itcoval  48650  setc1ocofval  49483