Theorem coeq1 5824

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-co 5650

This theorem is referenced by:  coeq1i  5826  coeq1d  5828  coi2  6239  funcoeqres  6834  wrecseq123  8295  ereq1  8681  domssex2  9107  wemapwe  9657  dfttrcl2  9684  updjud  9894  seqf1olem2  14014  seqf1o  14015  relexpsucnnl  15003  isps  18534  pwsco1mhm  18766  frmdup3  18801  efmndov  18815  symggrplem  18818  smndex1mndlem  18843  smndex1mnd  18844  pmtr3ncom  19412  psgnunilem1  19430  frgpup3  19715  gsumval3  19844  rngcinv  20553  ringcinv  20587  frgpcyg  21490  frlmup4  21717  evlseu  21997  evlsval2  22001  selvval  22029  evls1val  22214  evls1sca  22217  evl1val  22223  mpfpf1  22245  pf1mpf  22246  pf1ind  22249  xkococnlem  23553  xkococn  23554  cnmpt1k  23576  cnmptkk  23577  xkofvcn  23578  qtopeu  23610  qtophmeo  23711  utop2nei  24145  cncombf  25566  dgrcolem2  26187  dgrco  26188  motplusg  28476  hocsubdir  31721  hoddi  31926  opsqrlem1  32076  1arithidom  33515  smatfval  33792  msubco  35525  coideq  38242  trljco  40741  tgrpov  40749  tendovalco  40766  erngmul  40807  erngmul-rN  40815  cdlemksv  40845  cdlemkuu  40896  cdlemk41  40921  cdleml5N  40981  cdleml9  40985  dvamulr  41013  dvavadd  41016  dvhmulr  41087  dvhvscacbv  41099  dvhvscaval  41100  dih1dimatlem0  41329  dihjatcclem4  41422  evlsval3  42554  diophrw  42754  eldioph2  42757  diophren  42808  mendmulr  43180  fundcmpsurinjpreimafv  47413  rngcinvALTV  48268  ringcinvALTV  48302  itcoval  48654  setc1ocofval  49487