Theorem coeq1 5796

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3897   ∘ ccom 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914  df-br 5090  df-opab 5152  df-co 5623

This theorem is referenced by:  coeq1i  5798  coeq1d  5800  coi2  6211  funcoeqres  6794  wrecseq123  8243  ereq1  8629  domssex2  9050  wemapwe  9587  dfttrcl2  9614  updjud  9827  seqf1olem2  13949  seqf1o  13950  relexpsucnnl  14937  isps  18474  pwsco1mhm  18740  frmdup3  18775  efmndov  18789  symggrplem  18792  smndex1mndlem  18817  smndex1mnd  18818  pmtr3ncom  19387  psgnunilem1  19405  frgpup3  19690  gsumval3  19819  rngcinv  20552  ringcinv  20586  frgpcyg  21510  frlmup4  21738  evlseu  22018  evlsval2  22022  selvval  22050  evls1val  22235  evls1sca  22238  evl1val  22244  mpfpf1  22266  pf1mpf  22267  pf1ind  22270  xkococnlem  23574  xkococn  23575  cnmpt1k  23597  cnmptkk  23598  xkofvcn  23599  qtopeu  23631  qtophmeo  23732  utop2nei  24165  cncombf  25586  dgrcolem2  26207  dgrco  26208  motplusg  28520  hocsubdir  31765  hoddi  31970  opsqrlem1  32120  1arithidom  33502  mplvrpmga  33575  mplvrpmrhm  33577  issply  33584  smatfval  33808  msubco  35575  coideq  38293  trljco  40849  tgrpov  40857  tendovalco  40874  erngmul  40915  erngmul-rN  40923  cdlemksv  40953  cdlemkuu  41004  cdlemk41  41029  cdleml5N  41089  cdleml9  41093  dvamulr  41121  dvavadd  41124  dvhmulr  41195  dvhvscacbv  41207  dvhvscaval  41208  dih1dimatlem0  41437  dihjatcclem4  41530  evlsval3  42662  diophrw  42862  eldioph2  42865  diophren  42916  mendmulr  43287  fundcmpsurinjpreimafv  47518  rngcinvALTV  48386  ringcinvALTV  48420  itcoval  48772  setc1ocofval  49605