Theorem coeq2 5869

Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)

Assertion

Ref	Expression
coeq2	⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

Proof of Theorem coeq2

Step	Hyp	Ref	Expression
1		coss2 5867	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))
2		coss2 5867	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴))
3	1, 2	anim12i 613	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴)))
4		eqss 3999	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3999	. 2 ⊢ ((𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) ↔ ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴)))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-co 5694

This theorem is referenced by:  coeq2i  5871  coeq2d  5873  coi2  6283  f1eqcocnv  7321  ereq1  8752  dfttrcl2  9764  seqf1olem2  14083  seqf1o  14084  relexpsucnnr  15064  isps  18613  pwsco2mhm  18846  gsumwmhm  18858  frmdgsum  18875  frmdup1  18877  frmdup2  18878  efmndov  18894  symggrplem  18897  smndex1mndlem  18922  smndex1mnd  18923  pmtr3ncom  19493  psgnunilem1  19511  frgpuplem  19790  frgpupf  19791  frgpupval  19792  gsumval3eu  19922  gsumval3lem2  19924  rngcinv  20637  ringcinv  20671  selvval  22139  rhmmpl  22387  rhmply1vr1  22391  rhmply1vsca  22392  kgencn2  23565  upxp  23631  uptx  23633  txcn  23634  xkococnlem  23667  xkococn  23668  cnmptk1  23689  cnmptkk  23691  xkofvcn  23692  imasdsf1olem  24383  pi1cof  25092  pi1coval  25093  elovolmr  25511  ovoliunlem3  25539  ismbf1  25659  motplusg  28550  hocsubdir  31804  hoddi  32009  lnopco0i  32023  opsqrlem1  32159  pjsdi2i  32176  pjin2i  32212  pjclem1  32214  symgfcoeu  33102  1arithidomlem1  33563  1arithidom  33565  eulerpartgbij  34374  cvmliftmo  35289  cvmliftlem14  35302  cvmliftiota  35306  cvmlift2lem13  35320  cvmlift2  35321  cvmliftphtlem  35322  cvmlift3lem2  35325  cvmlift3lem6  35329  cvmlift3lem7  35330  cvmlift3lem9  35332  cvmlift3  35333  msubco  35536  ftc1anclem8  37707  upixp  37736  coideq  38248  xrneq1  38378  xrneq2  38381  trlcoat  40725  trljco  40742  tgrpov  40750  tendovalco  40767  erngmul  40808  erngmul-rN  40816  dvamulr  41014  dvavadd  41017  dvhmulr  41088  dihjatcclem4  41423  rhmpsr  42562  mendmulr  43196  hoiprodcl2  46570  ovnlecvr  46573  ovncvrrp  46579  ovnsubaddlem2  46586  ovncvr2  46626  opnvonmbllem1  46647  opnvonmbl  46649  ovolval4lem2  46665  ovolval5lem2  46668  ovolval5lem3  46669  ovolval5  46670  ovnovollem2  46672  rngcinvALTV  48192  ringcinvALTV  48226  itcoval1  48584  itcoval2  48585  itcoval3  48586  itcovalsucov  48589