Theorem coeq2 5838

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-br 5120  df-opab 5182  df-co 5663

This theorem is referenced by:  coeq2i  5840  coeq2d  5842  coi2  6252  f1eqcocnv  7294  ereq1  8726  dfttrcl2  9738  seqf1olem2  14060  seqf1o  14061  relexpsucnnr  15044  isps  18578  pwsco2mhm  18811  gsumwmhm  18823  frmdgsum  18840  frmdup1  18842  frmdup2  18843  efmndov  18859  symggrplem  18862  smndex1mndlem  18887  smndex1mnd  18888  pmtr3ncom  19456  psgnunilem1  19474  frgpuplem  19753  frgpupf  19754  frgpupval  19755  gsumval3eu  19885  gsumval3lem2  19887  rngcinv  20597  ringcinv  20631  selvval  22073  rhmmpl  22321  rhmply1vr1  22325  rhmply1vsca  22326  kgencn2  23495  upxp  23561  uptx  23563  txcn  23564  xkococnlem  23597  xkococn  23598  cnmptk1  23619  cnmptkk  23621  xkofvcn  23622  imasdsf1olem  24312  pi1cof  25010  pi1coval  25011  elovolmr  25429  ovoliunlem3  25457  ismbf1  25577  motplusg  28521  hocsubdir  31766  hoddi  31971  lnopco0i  31985  opsqrlem1  32121  pjsdi2i  32138  pjin2i  32174  pjclem1  32176  symgfcoeu  33093  1arithidomlem1  33550  1arithidom  33552  eulerpartgbij  34404  cvmliftmo  35306  cvmliftlem14  35319  cvmliftiota  35323  cvmlift2lem13  35337  cvmlift2  35338  cvmliftphtlem  35339  cvmlift3lem2  35342  cvmlift3lem6  35346  cvmlift3lem7  35347  cvmlift3lem9  35349  cvmlift3  35350  msubco  35553  ftc1anclem8  37724  upixp  37753  coideq  38265  xrneq1  38395  xrneq2  38398  trlcoat  40742  trljco  40759  tgrpov  40767  tendovalco  40784  erngmul  40825  erngmul-rN  40833  dvamulr  41031  dvavadd  41034  dvhmulr  41105  dihjatcclem4  41440  rhmpsr  42575  mendmulr  43208  hoiprodcl2  46584  ovnlecvr  46587  ovncvrrp  46593  ovnsubaddlem2  46600  ovncvr2  46640  opnvonmbllem1  46661  opnvonmbl  46663  ovolval4lem2  46679  ovolval5lem2  46682  ovolval5lem3  46683  ovolval5  46684  ovnovollem2  46686  rngcinvALTV  48251  ringcinvALTV  48285  itcoval1  48643  itcoval2  48644  itcoval3  48645  itcovalsucov  48648