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 5625

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3916  df-br 5096  df-opab 5158  df-co 5630

This theorem is referenced by:  coeq2i  5807  coeq2d  5809  coi2  6219  f1eqcocnv  7244  ereq1  8638  dfttrcl2  9624  seqf1olem2  13959  seqf1o  13960  relexpsucnnr  14942  isps  18484  pwsco2mhm  18751  gsumwmhm  18763  frmdgsum  18780  frmdup1  18782  frmdup2  18783  efmndov  18799  symggrplem  18802  smndex1mndlem  18827  smndex1mnd  18828  pmtr3ncom  19397  psgnunilem1  19415  frgpuplem  19694  frgpupf  19695  frgpupval  19696  gsumval3eu  19826  gsumval3lem2  19828  rngcinv  20562  ringcinv  20596  selvval  22060  rhmmpl  22308  rhmply1vr1  22312  rhmply1vsca  22313  kgencn2  23482  upxp  23548  uptx  23550  txcn  23551  xkococnlem  23584  xkococn  23585  cnmptk1  23606  cnmptkk  23608  xkofvcn  23609  imasdsf1olem  24298  pi1cof  24996  pi1coval  24997  elovolmr  25414  ovoliunlem3  25442  ismbf1  25562  motplusg  28530  hocsubdir  31776  hoddi  31981  lnopco0i  31995  opsqrlem1  32131  pjsdi2i  32148  pjin2i  32184  pjclem1  32186  symgfcoeu  33062  1arithidomlem1  33511  1arithidom  33513  mplvrpmfgalem  33585  mplvrpmga  33586  mplvrpmmhm  33587  mplvrpmrhm  33588  splysubrg  33594  issply  33595  eulerpartgbij  34396  cvmliftmo  35339  cvmliftlem14  35352  cvmliftiota  35356  cvmlift2lem13  35370  cvmlift2  35371  cvmliftphtlem  35372  cvmlift3lem2  35375  cvmlift3lem6  35379  cvmlift3lem7  35380  cvmlift3lem9  35382  cvmlift3  35383  msubco  35586  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  42660  mendmulr  43291  hoiprodcl2  46667  ovnlecvr  46670  ovncvrrp  46676  ovnsubaddlem2  46683  ovncvr2  46723  opnvonmbllem1  46744  opnvonmbl  46746  ovolval4lem2  46762  ovolval5lem2  46765  ovolval5lem3  46766  ovolval5  46767  ovnovollem2  46769  rngcinvALTV  48390  ringcinvALTV  48424  itcoval1  48778  itcoval2  48779  itcoval3  48780  itcovalsucov  48783