Theorem coeq1 5844

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ⊆ wss 3913   ∘ ccom 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-br 5114  df-opab 5178  df-co 5671

This theorem is referenced by:  coeq1i  5846  coeq1d  5848  coi2  6266  funcoeqres  6853  wrecseq123  8310  ereq1  8702  domssex2  9125  wemapwe  9666  dfttrcl2  9693  updjud  9920  seqf1olem2  14078  seqf1o  14079  relexpsucnnl  15067  isps  18624  pwsco1mhm  18891  frmdup3  18926  efmndov  18940  symggrplem  18943  smndex1mndlem  18971  smndex1mnd  18972  pmtr3ncom  19545  psgnunilem1  19563  frgpup3  19848  gsumval3  19977  rngcinv  20722  ringcinv  20756  frgpcyg  21692  frlmup4  21920  evlseu  22203  evlsval2  22207  evlsval3  22209  selvval  22240  evls1val  22449  evls1sca  22452  evl1val  22458  mpfpf1  22480  pf1mpf  22481  pf1ind  22484  xkococnlem  23785  xkococn  23786  cnmpt1k  23808  cnmptkk  23809  xkofvcn  23810  qtopeu  23842  qtophmeo  23943  utop2nei  24376  cncombf  25786  dgrcolem2  26400  dgrco  26401  motplusg  28777  hocsubdir  32078  hoddi  32283  opsqrlem1  32433  1arithidom  33772  mplvrpmga  33880  mplvrpmrhm  33882  issply  33896  smatfval  34130  msubco  35922  coideq  38787  trljco  41404  tgrpov  41412  tendovalco  41429  erngmul  41470  erngmul-rN  41478  cdlemksv  41508  cdlemkuu  41559  cdlemk41  41584  cdleml5N  41644  cdleml9  41648  dvamulr  41676  dvavadd  41679  dvhmulr  41750  dvhvscacbv  41762  dvhvscaval  41763  dih1dimatlem0  41992  dihjatcclem4  42085  diophrw  43382  eldioph2  43385  diophren  43432  mendmulr  43803  fundcmpsurinjpreimafv  48046  rngcinvALTV  48930  ringcinvALTV  48964  itcoval  49326  setc1ocofval  50157