Theorem coeq2 5805

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3899   ∘ ccom 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ss 3916  df-br 5097  df-opab 5159  df-co 5631

This theorem is referenced by:  coeq2i  5807  coeq2d  5809  coi2  6220  f1eqcocnv  7245  ereq1  8640  dfttrcl2  9631  seqf1olem2  13963  seqf1o  13964  relexpsucnnr  14946  isps  18489  pwsco2mhm  18756  gsumwmhm  18768  frmdgsum  18785  frmdup1  18787  frmdup2  18788  efmndov  18804  symggrplem  18807  smndex1mndlem  18832  smndex1mnd  18833  pmtr3ncom  19402  psgnunilem1  19420  frgpuplem  19699  frgpupf  19700  frgpupval  19701  gsumval3eu  19831  gsumval3lem2  19833  rngcinv  20568  ringcinv  20602  selvval  22076  rhmmpl  22325  rhmply1vr1  22329  rhmply1vsca  22330  kgencn2  23499  upxp  23565  uptx  23567  txcn  23568  xkococnlem  23601  xkococn  23602  cnmptk1  23623  cnmptkk  23625  xkofvcn  23626  imasdsf1olem  24315  pi1cof  25013  pi1coval  25014  elovolmr  25431  ovoliunlem3  25459  ismbf1  25579  motplusg  28563  hocsubdir  31809  hoddi  32014  lnopco0i  32028  opsqrlem1  32164  pjsdi2i  32181  pjin2i  32217  pjclem1  32219  symgfcoeu  33113  1arithidomlem1  33565  1arithidom  33567  mplvrpmfgalem  33658  mplvrpmga  33659  mplvrpmmhm  33660  mplvrpmrhm  33661  splysubrg  33667  issply  33668  eulerpartgbij  34478  cvmliftmo  35427  cvmliftlem14  35440  cvmliftiota  35444  cvmlift2lem13  35458  cvmlift2  35459  cvmliftphtlem  35460  cvmlift3lem2  35463  cvmlift3lem6  35467  cvmlift3lem7  35468  cvmlift3lem9  35470  cvmlift3  35471  msubco  35674  ftc1anclem8  37840  upixp  37869  coideq  38383  xrneq1  38520  xrneq2  38523  trlcoat  40922  trljco  40939  tgrpov  40947  tendovalco  40964  erngmul  41005  erngmul-rN  41013  dvamulr  41211  dvavadd  41214  dvhmulr  41285  dihjatcclem4  41620  rhmpsr  42747  mendmulr  43368  hoiprodcl2  46741  ovnlecvr  46744  ovncvrrp  46750  ovnsubaddlem2  46757  ovncvr2  46797  opnvonmbllem1  46818  opnvonmbl  46820  ovolval4lem2  46836  ovolval5lem2  46839  ovolval5lem3  46840  ovolval5  46841  ovnovollem2  46843  rngcinvALTV  48464  ringcinvALTV  48498  itcoval1  48851  itcoval2  48852  itcoval3  48853  itcovalsucov  48856