Theorem coeq1 5766

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ⊆ wss 3887   ∘ ccom 5593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-br 5075  df-opab 5137  df-co 5598

This theorem is referenced by:  coeq1i  5768  coeq1d  5770  coi2  6167  funcoeqres  6747  wrecseq123  8130  ereq1  8505  domssex2  8924  wemapwe  9455  dfttrcl2  9482  updjud  9692  seqf1olem2  13763  seqf1o  13764  relexpsucnnl  14741  isps  18286  pwsco1mhm  18470  frmdup3  18506  efmndov  18520  symggrplem  18523  smndex1mndlem  18548  smndex1mnd  18549  pmtr3ncom  19083  psgnunilem1  19101  frgpup3  19384  gsumval3  19508  frgpcyg  20781  frlmup4  21008  evlseu  21293  evlsval2  21297  selvval  21328  evls1val  21486  evls1sca  21489  evl1val  21495  mpfpf1  21517  pf1mpf  21518  pf1ind  21521  xkococnlem  22810  xkococn  22811  cnmpt1k  22833  cnmptkk  22834  xkofvcn  22835  qtopeu  22867  qtophmeo  22968  utop2nei  23402  cncombf  24822  dgrcolem2  25435  dgrco  25436  motplusg  26903  hocsubdir  30147  hoddi  30352  opsqrlem1  30502  smatfval  31745  msubco  33493  coideq  36385  trljco  38754  tgrpov  38762  tendovalco  38779  erngmul  38820  erngmul-rN  38828  cdlemksv  38858  cdlemkuu  38909  cdlemk41  38934  cdleml5N  38994  cdleml9  38998  dvamulr  39026  dvavadd  39029  dvhmulr  39100  dvhvscacbv  39112  dvhvscaval  39113  dih1dimatlem0  39342  dihjatcclem4  39435  evlsval3  40272  diophrw  40581  eldioph2  40584  diophren  40635  mendmulr  41013  fundcmpsurinjpreimafv  44860  rngcinv  45539  rngcinvALTV  45551  ringcinv  45590  ringcinvALTV  45614  itcoval  46007