Theorem coeq2 5847

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5109  df-opab 5174  df-co 5667

This theorem is used by:  coeq2i  5849  coeq2d  5851  coi2  6286  f1eqcocnv  7340  ereq1  8763  dfttrcl2  9762  seqf1olem2  14225  seqf1o  14226  relexpsucnnr  15221  isps  18792  pwsco2mhm  19079  gsumwmhm  19091  frmdgsum  19108  frmdup1  19110  frmdup2  19111  efmndov  19127  symggrplem  19130  smndex1mndlem  19158  smndex1mnd  19159  pmtr3ncom  19740  psgnunilem1  19758  frgpuplem  20037  frgpupf  20038  frgpupval  20039  gsumval3eu  20169  gsumval3lem2  20171  rngcinv  20940  ringcinv  20974  selvval  22484  rhmmpl  22753  rhmply1vr1  22757  rhmply1vsca  22758  kgencn2  23931  upxp  23997  uptx  23999  txcn  24000  xkococnlem  24033  xkococn  24034  cnmptk1  24055  cnmptkk  24057  xkofvcn  24058  imasdsf1olem  24747  pi1cof  25435  pi1coval  25436  elovolmr  25852  ovoliunlem3  25880  ismbf1  26000  motplusg  29062  hocsubdir  32444  hoddi  32649  lnopco0i  32663  opsqrlem1  32799  pjsdi2i  32816  pjin2i  32852  pjclem1  32854  symgfcoeu  33742  1arithidomlem1  34171  1arithidom  34173  mplvrpmfgalem  34287  mplvrpmga  34288  mplvrpmmhm  34289  mplvrpmrhm  34290  splysubrg  34303  issply  34304  eulerpartgbij  35115  cvmliftmo  36257  cvmliftlem14  36270  cvmliftiota  36274  cvmlift2lem13  36288  cvmlift2  36289  cvmliftphtlem  36290  cvmlift3lem2  36293  cvmlift3lem6  36297  cvmlift3lem7  36298  cvmlift3lem9  36300  cvmlift3  36301  msubco  36504  coineq0  38208  ftc1anclem8  38886  upixp  38931  coideq  39446  xrneq1  39594  xrneq2  39597  shiftstableeq2  39681  trlcoat  42046  trljco  42063  tgrpov  42071  tendovalco  42088  erngmul  42129  erngmul-rN  42137  dvamulr  42335  dvavadd  42338  dvhmulr  42409  dihjatcclem4  42744  rhmpsr  43877  mendmulr  44447  hoiprodcl2  47838  ovnlecvr  47841  ovncvrrp  47847  ovnsubaddlem2  47854  ovncvr2  47894  opnvonmbllem1  47915  opnvonmbl  47917  ovolval4lem2  47933  ovolval5lem2  47936  ovolval5lem3  47937  ovolval5  47938  ovnovollem2  47940  rngcinvALTV  49646  ringcinvALTV  49680  itcoval1  50106  itcoval2  50107  itcoval3  50108  itcovalsucov  50111