Theorem coeq1 5711

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ⊆ wss 3853   ∘ ccom 5540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-br 5040  df-opab 5102  df-co 5545

This theorem is referenced by:  coeq1i  5713  coeq1d  5715  coi2  6107  funcoeqres  6669  ereq1  8376  domssex2  8784  wemapwe  9290  updjud  9515  seqf1olem2  13581  seqf1o  13582  relexpsucnnl  14558  isps  18028  pwsco1mhm  18212  frmdup3  18248  efmndov  18262  symggrplem  18265  smndex1mndlem  18290  smndex1mnd  18291  pmtr3ncom  18821  psgnunilem1  18839  frgpup3  19122  gsumval3  19246  frgpcyg  20492  frlmup4  20717  evlseu  20997  evlsval2  21001  selvval  21032  evls1val  21190  evls1sca  21193  evl1val  21199  mpfpf1  21221  pf1mpf  21222  pf1ind  21225  xkococnlem  22510  xkococn  22511  cnmpt1k  22533  cnmptkk  22534  xkofvcn  22535  qtopeu  22567  qtophmeo  22668  utop2nei  23102  cncombf  24509  dgrcolem2  25122  dgrco  25123  motplusg  26587  hocsubdir  29820  hoddi  30025  opsqrlem1  30175  smatfval  31413  msubco  33160  coideq  36071  trljco  38440  tgrpov  38448  tendovalco  38465  erngmul  38506  erngmul-rN  38514  cdlemksv  38544  cdlemkuu  38595  cdlemk41  38620  cdleml5N  38680  cdleml9  38684  dvamulr  38712  dvavadd  38715  dvhmulr  38786  dvhvscacbv  38798  dvhvscaval  38799  dih1dimatlem0  39028  dihjatcclem4  39121  evlsval3  39923  diophrw  40225  eldioph2  40228  diophren  40279  mendmulr  40657  fundcmpsurinjpreimafv  44476  rngcinv  45155  rngcinvALTV  45167  ringcinv  45206  ringcinvALTV  45230  itcoval  45623