Theorem coeq2 5883

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ⊆ wss 3976   ∘ ccom 5704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-co 5709

This theorem is referenced by:  coeq2i  5885  coeq2d  5887  coi2  6294  f1eqcocnv  7337  ereq1  8770  dfttrcl2  9793  seqf1olem2  14093  seqf1o  14094  relexpsucnnr  15074  isps  18638  pwsco2mhm  18868  gsumwmhm  18880  frmdgsum  18897  frmdup1  18899  frmdup2  18900  efmndov  18916  symggrplem  18919  smndex1mndlem  18944  smndex1mnd  18945  pmtr3ncom  19517  psgnunilem1  19535  frgpuplem  19814  frgpupf  19815  frgpupval  19816  gsumval3eu  19946  gsumval3lem2  19948  rngcinv  20659  ringcinv  20693  selvval  22162  rhmmpl  22408  rhmply1vr1  22412  rhmply1vsca  22413  kgencn2  23586  upxp  23652  uptx  23654  txcn  23655  xkococnlem  23688  xkococn  23689  cnmptk1  23710  cnmptkk  23712  xkofvcn  23713  imasdsf1olem  24404  pi1cof  25111  pi1coval  25112  elovolmr  25530  ovoliunlem3  25558  ismbf1  25678  motplusg  28568  hocsubdir  31817  hoddi  32022  lnopco0i  32036  opsqrlem1  32172  pjsdi2i  32189  pjin2i  32225  pjclem1  32227  symgfcoeu  33075  1arithidomlem1  33528  1arithidom  33530  eulerpartgbij  34337  cvmliftmo  35252  cvmliftlem14  35265  cvmliftiota  35269  cvmlift2lem13  35283  cvmlift2  35284  cvmliftphtlem  35285  cvmlift3lem2  35288  cvmlift3lem6  35292  cvmlift3lem7  35293  cvmlift3lem9  35295  cvmlift3  35296  msubco  35499  ftc1anclem8  37660  upixp  37689  coideq  38202  xrneq1  38333  xrneq2  38336  trlcoat  40680  trljco  40697  tgrpov  40705  tendovalco  40722  erngmul  40763  erngmul-rN  40771  dvamulr  40969  dvavadd  40972  dvhmulr  41043  dihjatcclem4  41378  rhmpsr  42507  mendmulr  43145  hoiprodcl2  46476  ovnlecvr  46479  ovncvrrp  46485  ovnsubaddlem2  46492  ovncvr2  46532  opnvonmbllem1  46553  opnvonmbl  46555  ovolval4lem2  46571  ovolval5lem2  46574  ovolval5lem3  46575  ovolval5  46576  ovnovollem2  46578  rngcinvALTV  47999  ringcinvALTV  48033  itcoval1  48397  itcoval2  48398  itcoval3  48399  itcovalsucov  48402