Theorem coeq1 5811

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

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

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 3928  df-br 5103  df-opab 5165  df-co 5640

This theorem is referenced by:  coeq1i  5813  coeq1d  5815  coi2  6224  funcoeqres  6813  wrecseq123  8269  ereq1  8655  domssex2  9078  wemapwe  9626  dfttrcl2  9653  updjud  9863  seqf1olem2  13983  seqf1o  13984  relexpsucnnl  14972  isps  18509  pwsco1mhm  18741  frmdup3  18776  efmndov  18790  symggrplem  18793  smndex1mndlem  18818  smndex1mnd  18819  pmtr3ncom  19389  psgnunilem1  19407  frgpup3  19692  gsumval3  19821  rngcinv  20557  ringcinv  20591  frgpcyg  21515  frlmup4  21743  evlseu  22023  evlsval2  22027  selvval  22055  evls1val  22240  evls1sca  22243  evl1val  22249  mpfpf1  22271  pf1mpf  22272  pf1ind  22275  xkococnlem  23579  xkococn  23580  cnmpt1k  23602  cnmptkk  23603  xkofvcn  23604  qtopeu  23636  qtophmeo  23737  utop2nei  24171  cncombf  25592  dgrcolem2  26213  dgrco  26214  motplusg  28522  hocsubdir  31764  hoddi  31969  opsqrlem1  32119  1arithidom  33501  smatfval  33778  msubco  35511  coideq  38228  trljco  40727  tgrpov  40735  tendovalco  40752  erngmul  40793  erngmul-rN  40801  cdlemksv  40831  cdlemkuu  40882  cdlemk41  40907  cdleml5N  40967  cdleml9  40971  dvamulr  40999  dvavadd  41002  dvhmulr  41073  dvhvscacbv  41085  dvhvscaval  41086  dih1dimatlem0  41315  dihjatcclem4  41408  evlsval3  42540  diophrw  42740  eldioph2  42743  diophren  42794  mendmulr  43166  fundcmpsurinjpreimafv  47402  rngcinvALTV  48257  ringcinvALTV  48291  itcoval  48643  setc1ocofval  49476