Theorem coeq1 5821

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

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

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 3931  df-br 5108  df-opab 5170  df-co 5647

This theorem is referenced by:  coeq1i  5823  coeq1d  5825  coi2  6236  funcoeqres  6831  wrecseq123  8292  ereq1  8678  domssex2  9101  wemapwe  9650  dfttrcl2  9677  updjud  9887  seqf1olem2  14007  seqf1o  14008  relexpsucnnl  14996  isps  18527  pwsco1mhm  18759  frmdup3  18794  efmndov  18808  symggrplem  18811  smndex1mndlem  18836  smndex1mnd  18837  pmtr3ncom  19405  psgnunilem1  19423  frgpup3  19708  gsumval3  19837  rngcinv  20546  ringcinv  20580  frgpcyg  21483  frlmup4  21710  evlseu  21990  evlsval2  21994  selvval  22022  evls1val  22207  evls1sca  22210  evl1val  22216  mpfpf1  22238  pf1mpf  22239  pf1ind  22242  xkococnlem  23546  xkococn  23547  cnmpt1k  23569  cnmptkk  23570  xkofvcn  23571  qtopeu  23603  qtophmeo  23704  utop2nei  24138  cncombf  25559  dgrcolem2  26180  dgrco  26181  motplusg  28469  hocsubdir  31714  hoddi  31919  opsqrlem1  32069  1arithidom  33508  smatfval  33785  msubco  35518  coideq  38235  trljco  40734  tgrpov  40742  tendovalco  40759  erngmul  40800  erngmul-rN  40808  cdlemksv  40838  cdlemkuu  40889  cdlemk41  40914  cdleml5N  40974  cdleml9  40978  dvamulr  41006  dvavadd  41009  dvhmulr  41080  dvhvscacbv  41092  dvhvscaval  41093  dih1dimatlem0  41322  dihjatcclem4  41415  evlsval3  42547  diophrw  42747  eldioph2  42750  diophren  42801  mendmulr  43173  fundcmpsurinjpreimafv  47409  rngcinvALTV  48264  ringcinvALTV  48298  itcoval  48650  setc1ocofval  49483