Theorem coeq2 5815

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3903   ∘ ccom 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-br 5101  df-opab 5163  df-co 5641

This theorem is referenced by:  coeq2i  5817  coeq2d  5819  coi2  6230  f1eqcocnv  7257  ereq1  8653  dfttrcl2  9645  seqf1olem2  13977  seqf1o  13978  relexpsucnnr  14960  isps  18503  pwsco2mhm  18770  gsumwmhm  18782  frmdgsum  18799  frmdup1  18801  frmdup2  18802  efmndov  18818  symggrplem  18821  smndex1mndlem  18846  smndex1mnd  18847  pmtr3ncom  19416  psgnunilem1  19434  frgpuplem  19713  frgpupf  19714  frgpupval  19715  gsumval3eu  19845  gsumval3lem2  19847  rngcinv  20582  ringcinv  20616  selvval  22090  rhmmpl  22339  rhmply1vr1  22343  rhmply1vsca  22344  kgencn2  23513  upxp  23579  uptx  23581  txcn  23582  xkococnlem  23615  xkococn  23616  cnmptk1  23637  cnmptkk  23639  xkofvcn  23640  imasdsf1olem  24329  pi1cof  25027  pi1coval  25028  elovolmr  25445  ovoliunlem3  25473  ismbf1  25593  motplusg  28626  hocsubdir  31873  hoddi  32078  lnopco0i  32092  opsqrlem1  32228  pjsdi2i  32245  pjin2i  32281  pjclem1  32283  symgfcoeu  33176  1arithidomlem1  33628  1arithidom  33630  mplvrpmfgalem  33721  mplvrpmga  33722  mplvrpmmhm  33723  mplvrpmrhm  33724  splysubrg  33737  issply  33738  eulerpartgbij  34550  cvmliftmo  35500  cvmliftlem14  35513  cvmliftiota  35517  cvmlift2lem13  35531  cvmlift2  35532  cvmliftphtlem  35533  cvmlift3lem2  35536  cvmlift3lem6  35540  cvmlift3lem7  35541  cvmlift3lem9  35543  cvmlift3  35544  msubco  35747  ftc1anclem8  37951  upixp  37980  coideq  38499  xrneq1  38647  xrneq2  38650  shiftstableeq2  38734  trlcoat  41099  trljco  41116  tgrpov  41124  tendovalco  41141  erngmul  41182  erngmul-rN  41190  dvamulr  41388  dvavadd  41391  dvhmulr  41462  dihjatcclem4  41797  rhmpsr  42920  mendmulr  43541  hoiprodcl2  46913  ovnlecvr  46916  ovncvrrp  46922  ovnsubaddlem2  46929  ovncvr2  46969  opnvonmbllem1  46990  opnvonmbl  46992  ovolval4lem2  47008  ovolval5lem2  47011  ovolval5lem3  47012  ovolval5  47013  ovnovollem2  47015  rngcinvALTV  48636  ringcinvALTV  48670  itcoval1  49023  itcoval2  49024  itcoval3  49025  itcovalsucov  49028