Theorem coeq1 5784

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ⊆ wss 3896   ∘ ccom 5609

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-in 3903  df-ss 3913  df-br 5086  df-opab 5148  df-co 5614

This theorem is referenced by:  coeq1i  5786  coeq1d  5788  coi2  6186  funcoeqres  6782  wrecseq123  8175  ereq1  8551  domssex2  8977  wemapwe  9523  dfttrcl2  9550  updjud  9760  seqf1olem2  13833  seqf1o  13834  relexpsucnnl  14810  isps  18353  pwsco1mhm  18537  frmdup3  18573  efmndov  18587  symggrplem  18590  smndex1mndlem  18615  smndex1mnd  18616  pmtr3ncom  19150  psgnunilem1  19168  frgpup3  19451  gsumval3  19575  frgpcyg  20852  frlmup4  21079  evlseu  21364  evlsval2  21368  selvval  21399  evls1val  21557  evls1sca  21560  evl1val  21566  mpfpf1  21588  pf1mpf  21589  pf1ind  21592  xkococnlem  22881  xkococn  22882  cnmpt1k  22904  cnmptkk  22905  xkofvcn  22906  qtopeu  22938  qtophmeo  23039  utop2nei  23473  cncombf  24893  dgrcolem2  25506  dgrco  25507  motplusg  27011  hocsubdir  30255  hoddi  30460  opsqrlem1  30610  smatfval  31851  msubco  33599  coideq  36466  trljco  38966  tgrpov  38974  tendovalco  38991  erngmul  39032  erngmul-rN  39040  cdlemksv  39070  cdlemkuu  39121  cdlemk41  39146  cdleml5N  39206  cdleml9  39210  dvamulr  39238  dvavadd  39241  dvhmulr  39312  dvhvscacbv  39324  dvhvscaval  39325  dih1dimatlem0  39554  dihjatcclem4  39647  evlsval3  40482  diophrw  40791  eldioph2  40794  diophren  40845  mendmulr  41224  fundcmpsurinjpreimafv  45119  rngcinv  45798  rngcinvALTV  45810  ringcinv  45849  ringcinvALTV  45873  itcoval  46266