Theorem coeq2 5797

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

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

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914  df-br 5090  df-opab 5152  df-co 5623

This theorem is referenced by:  coeq2i  5799  coeq2d  5801  coi2  6211  f1eqcocnv  7235  ereq1  8629  dfttrcl2  9614  seqf1olem2  13949  seqf1o  13950  relexpsucnnr  14932  isps  18474  pwsco2mhm  18741  gsumwmhm  18753  frmdgsum  18770  frmdup1  18772  frmdup2  18773  efmndov  18789  symggrplem  18792  smndex1mndlem  18817  smndex1mnd  18818  pmtr3ncom  19387  psgnunilem1  19405  frgpuplem  19684  frgpupf  19685  frgpupval  19686  gsumval3eu  19816  gsumval3lem2  19818  rngcinv  20552  ringcinv  20586  selvval  22050  rhmmpl  22298  rhmply1vr1  22302  rhmply1vsca  22303  kgencn2  23472  upxp  23538  uptx  23540  txcn  23541  xkococnlem  23574  xkococn  23575  cnmptk1  23596  cnmptkk  23598  xkofvcn  23599  imasdsf1olem  24288  pi1cof  24986  pi1coval  24987  elovolmr  25404  ovoliunlem3  25432  ismbf1  25552  motplusg  28520  hocsubdir  31765  hoddi  31970  lnopco0i  31984  opsqrlem1  32120  pjsdi2i  32137  pjin2i  32173  pjclem1  32175  symgfcoeu  33051  1arithidomlem1  33500  1arithidom  33502  mplvrpmfgalem  33574  mplvrpmga  33575  mplvrpmmhm  33576  mplvrpmrhm  33577  splysubrg  33583  issply  33584  eulerpartgbij  34385  cvmliftmo  35328  cvmliftlem14  35341  cvmliftiota  35345  cvmlift2lem13  35359  cvmlift2  35360  cvmliftphtlem  35361  cvmlift3lem2  35364  cvmlift3lem6  35368  cvmlift3lem7  35369  cvmlift3lem9  35371  cvmlift3  35372  msubco  35575  ftc1anclem8  37750  upixp  37779  coideq  38293  xrneq1  38430  xrneq2  38433  trlcoat  40832  trljco  40849  tgrpov  40857  tendovalco  40874  erngmul  40915  erngmul-rN  40923  dvamulr  41121  dvavadd  41124  dvhmulr  41195  dihjatcclem4  41530  rhmpsr  42655  mendmulr  43287  hoiprodcl2  46663  ovnlecvr  46666  ovncvrrp  46672  ovnsubaddlem2  46679  ovncvr2  46719  opnvonmbllem1  46740  opnvonmbl  46742  ovolval4lem2  46758  ovolval5lem2  46761  ovolval5lem3  46762  ovolval5  46763  ovnovollem2  46765  rngcinvALTV  48386  ringcinvALTV  48420  itcoval1  48774  itcoval2  48775  itcoval3  48776  itcovalsucov  48779