Theorem coeq1 5882

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ⊆ wss 3976   ∘ ccom 5704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-co 5709

This theorem is referenced by:  coeq1i  5884  coeq1d  5886  coi2  6294  funcoeqres  6893  wrecseq123  8355  ereq1  8770  domssex2  9203  wemapwe  9766  dfttrcl2  9793  updjud  10003  seqf1olem2  14093  seqf1o  14094  relexpsucnnl  15079  isps  18638  pwsco1mhm  18867  frmdup3  18902  efmndov  18916  symggrplem  18919  smndex1mndlem  18944  smndex1mnd  18945  pmtr3ncom  19517  psgnunilem1  19535  frgpup3  19820  gsumval3  19949  rngcinv  20659  ringcinv  20693  frgpcyg  21615  frlmup4  21844  evlseu  22130  evlsval2  22134  selvval  22162  evls1val  22345  evls1sca  22348  evl1val  22354  mpfpf1  22376  pf1mpf  22377  pf1ind  22380  xkococnlem  23688  xkococn  23689  cnmpt1k  23711  cnmptkk  23712  xkofvcn  23713  qtopeu  23745  qtophmeo  23846  utop2nei  24280  cncombf  25712  dgrcolem2  26334  dgrco  26335  motplusg  28568  hocsubdir  31817  hoddi  32022  opsqrlem1  32172  1arithidom  33530  smatfval  33741  msubco  35499  coideq  38202  trljco  40697  tgrpov  40705  tendovalco  40722  erngmul  40763  erngmul-rN  40771  cdlemksv  40801  cdlemkuu  40852  cdlemk41  40877  cdleml5N  40937  cdleml9  40941  dvamulr  40969  dvavadd  40972  dvhmulr  41043  dvhvscacbv  41055  dvhvscaval  41056  dih1dimatlem0  41285  dihjatcclem4  41378  evlsval3  42514  diophrw  42715  eldioph2  42718  diophren  42769  mendmulr  43145  fundcmpsurinjpreimafv  47282  rngcinvALTV  47999  ringcinvALTV  48033  itcoval  48395