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 625	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴)))
4		eqss 3946	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3946	. 2 ⊢ ((𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) ↔ ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴)))
6	3, 4, 5	3imtr4i 295	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3899   ∘ ccom 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-br 5104  df-opab 5168  df-co 5664

This theorem is used by:  coeq2i  5840  coeq2d  5842  coi2  6260  f1eqcocnv  7303  ereq1  8705  dfttrcl2  9704  seqf1olem2  14107  seqf1o  14108  relexpsucnnr  15099  isps  18657  pwsco2mhm  18943  gsumwmhm  18955  frmdgsum  18972  frmdup1  18974  frmdup2  18975  efmndov  18991  symggrplem  18994  smndex1mndlem  19022  smndex1mnd  19023  pmtr3ncom  19603  psgnunilem1  19621  frgpuplem  19900  frgpupf  19901  frgpupval  19902  gsumval3eu  20032  gsumval3lem2  20034  rngcinv  20800  ringcinv  20834  selvval  22337  rhmmpl  22606  rhmply1vr1  22610  rhmply1vsca  22611  kgencn2  23784  upxp  23850  uptx  23852  txcn  23853  xkococnlem  23886  xkococn  23887  cnmptk1  23908  cnmptkk  23910  xkofvcn  23911  imasdsf1olem  24600  pi1cof  25288  pi1coval  25289  elovolmr  25705  ovoliunlem3  25733  ismbf1  25853  motplusg  28885  hocsubdir  32267  hoddi  32472  lnopco0i  32486  opsqrlem1  32622  pjsdi2i  32639  pjin2i  32675  pjclem1  32677  symgfcoeu  33523  1arithidomlem1  33946  1arithidom  33948  mplvrpmfgalem  34055  mplvrpmga  34056  mplvrpmmhm  34057  mplvrpmrhm  34058  splysubrg  34071  issply  34072  eulerpartgbij  34884  cvmliftmo  35864  cvmliftlem14  35877  cvmliftiota  35881  cvmlift2lem13  35895  cvmlift2  35896  cvmliftphtlem  35897  cvmlift3lem2  35900  cvmlift3lem6  35904  cvmlift3lem7  35905  cvmlift3lem9  35907  cvmlift3  35908  msubco  36111  ftc1anclem8  38450  upixp  38480  coideq  38997  xrneq1  39145  xrneq2  39148  shiftstableeq2  39232  trlcoat  41597  trljco  41614  tgrpov  41622  tendovalco  41639  erngmul  41680  erngmul-rN  41688  dvamulr  41886  dvavadd  41889  dvhmulr  41960  dihjatcclem4  42295  rhmpsr  43430  mendmulr  44026  hoiprodcl2  47384  ovnlecvr  47387  ovncvrrp  47393  ovnsubaddlem2  47400  ovncvr2  47440  opnvonmbllem1  47461  opnvonmbl  47463  ovolval4lem2  47479  ovolval5lem2  47482  ovolval5lem3  47483  ovolval5  47484  ovnovollem2  47486  rngcinvALTV  49192  ringcinvALTV  49226  itcoval1  49594  itcoval2  49595  itcoval3  49596  itcovalsucov  49599