Theorem coeq1 5731

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ⊆ wss 3939   ∘ ccom 5562

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-in 3946  df-ss 3955  df-br 5070  df-opab 5132  df-co 5567

This theorem is referenced by:  coeq1i  5733  coeq1d  5735  coi2  6119  funcoeqres  6648  ereq1  8299  domssex2  8680  wemapwe  9163  updjud  9366  seqf1olem2  13413  seqf1o  13414  relexpsucnnl  14394  isps  17815  pwsco1mhm  17999  frmdup3  18035  efmndov  18049  symggrplem  18052  smndex1mndlem  18077  smndex1mnd  18078  pmtr3ncom  18606  psgnunilem1  18624  frgpup3  18907  gsumval3  19030  evlseu  20299  evlsval2  20303  selvval  20334  evls1val  20486  evls1sca  20489  evl1val  20495  mpfpf1  20517  pf1mpf  20518  pf1ind  20521  frgpcyg  20723  frlmup4  20948  xkococnlem  22270  xkococn  22271  cnmpt1k  22293  cnmptkk  22294  xkofvcn  22295  qtopeu  22327  qtophmeo  22428  utop2nei  22862  cncombf  24262  dgrcolem2  24867  dgrco  24868  motplusg  26331  hocsubdir  29565  hoddi  29770  opsqrlem1  29920  smatfval  31064  msubco  32782  coideq  35511  trljco  37880  tgrpov  37888  tendovalco  37905  erngmul  37946  erngmul-rN  37954  cdlemksv  37984  cdlemkuu  38035  cdlemk41  38060  cdleml5N  38120  cdleml9  38124  dvamulr  38152  dvavadd  38155  dvhmulr  38226  dvhvscacbv  38238  dvhvscaval  38239  dih1dimatlem0  38468  dihjatcclem4  38561  diophrw  39362  eldioph2  39365  diophren  39416  mendmulr  39794  fundcmpsurinjpreimafv  43575  rngcinv  44259  rngcinvALTV  44271  ringcinv  44310  ringcinvALTV  44334