Theorem coeq1 5799

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ⊆ wss 3883   ∘ ccom 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900  df-br 5073  df-opab 5135  df-co 5627

This theorem is referenced by:  coeq1i  5801  coeq1d  5803  coi2  6215  funcoeqres  6798  wrecseq123  8253  ereq1  8641  domssex2  9065  wemapwe  9609  dfttrcl2  9636  updjud  9849  seqf1olem2  13995  seqf1o  13996  relexpsucnnl  14983  isps  18525  pwsco1mhm  18791  frmdup3  18826  efmndov  18840  symggrplem  18843  smndex1mndlem  18871  smndex1mnd  18872  pmtr3ncom  19441  psgnunilem1  19459  frgpup3  19744  gsumval3  19873  rngcinv  20609  ringcinv  20643  frgpcyg  21548  frlmup4  21776  evlseu  22059  evlsval2  22063  evlsval3  22065  selvval  22096  evls1val  22306  evls1sca  22309  evl1val  22315  mpfpf1  22337  pf1mpf  22338  pf1ind  22341  xkococnlem  23642  xkococn  23643  cnmpt1k  23665  cnmptkk  23666  xkofvcn  23667  qtopeu  23699  qtophmeo  23800  utop2nei  24233  cncombf  25643  dgrcolem2  26257  dgrco  26258  motplusg  28628  hocsubdir  31874  hoddi  32079  opsqrlem1  32229  1arithidom  33620  mplvrpmga  33729  mplvrpmrhm  33731  issply  33745  smatfval  33979  msubco  35759  coideq  38615  trljco  41232  tgrpov  41240  tendovalco  41257  erngmul  41298  erngmul-rN  41306  cdlemksv  41336  cdlemkuu  41387  cdlemk41  41412  cdleml5N  41472  cdleml9  41476  dvamulr  41504  dvavadd  41507  dvhmulr  41578  dvhvscacbv  41590  dvhvscaval  41591  dih1dimatlem0  41820  dihjatcclem4  41913  diophrw  43208  eldioph2  43211  diophren  43258  mendmulr  43629  fundcmpsurinjpreimafv  47883  rngcinvALTV  48767  ringcinvALTV  48801  itcoval  49152  setc1ocofval  49984