Theorem coeq1 5755

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ⊆ wss 3883   ∘ ccom 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071  df-opab 5133  df-co 5589

This theorem is referenced by:  coeq1i  5757  coeq1d  5759  coi2  6156  funcoeqres  6730  wrecseq123  8101  ereq1  8463  domssex2  8873  wemapwe  9385  updjud  9623  seqf1olem2  13691  seqf1o  13692  relexpsucnnl  14669  isps  18201  pwsco1mhm  18385  frmdup3  18421  efmndov  18435  symggrplem  18438  smndex1mndlem  18463  smndex1mnd  18464  pmtr3ncom  18998  psgnunilem1  19016  frgpup3  19299  gsumval3  19423  frgpcyg  20693  frlmup4  20918  evlseu  21203  evlsval2  21207  selvval  21238  evls1val  21396  evls1sca  21399  evl1val  21405  mpfpf1  21427  pf1mpf  21428  pf1ind  21431  xkococnlem  22718  xkococn  22719  cnmpt1k  22741  cnmptkk  22742  xkofvcn  22743  qtopeu  22775  qtophmeo  22876  utop2nei  23310  cncombf  24727  dgrcolem2  25340  dgrco  25341  motplusg  26807  hocsubdir  30048  hoddi  30253  opsqrlem1  30403  smatfval  31647  msubco  33393  dfttrcl2  33710  coideq  36312  trljco  38681  tgrpov  38689  tendovalco  38706  erngmul  38747  erngmul-rN  38755  cdlemksv  38785  cdlemkuu  38836  cdlemk41  38861  cdleml5N  38921  cdleml9  38925  dvamulr  38953  dvavadd  38956  dvhmulr  39027  dvhvscacbv  39039  dvhvscaval  39040  dih1dimatlem0  39269  dihjatcclem4  39362  evlsval3  40195  diophrw  40497  eldioph2  40500  diophren  40551  mendmulr  40929  fundcmpsurinjpreimafv  44748  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  itcoval  45895