Theorem coeq2 5836

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 5834	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))
2		coss2 5834	. . 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 5655

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-br 5104  df-opab 5168  df-co 5660

This theorem is used by:  coeq2i  5838  coeq2d  5840  coi2  6265  f1eqcocnv  7309  ereq1  8725  dfttrcl2  9725  seqf1olem2  14185  seqf1o  14186  relexpsucnnr  15178  isps  18742  pwsco2mhm  19029  gsumwmhm  19041  frmdgsum  19058  frmdup1  19060  frmdup2  19061  efmndov  19077  symggrplem  19080  smndex1mndlem  19108  smndex1mnd  19109  pmtr3ncom  19689  psgnunilem1  19707  frgpuplem  19986  frgpupf  19987  frgpupval  19988  gsumval3eu  20118  gsumval3lem2  20120  rngcinv  20889  ringcinv  20923  selvval  22429  rhmmpl  22698  rhmply1vr1  22702  rhmply1vsca  22703  kgencn2  23876  upxp  23942  uptx  23944  txcn  23945  xkococnlem  23978  xkococn  23979  cnmptk1  24000  cnmptkk  24002  xkofvcn  24003  imasdsf1olem  24692  pi1cof  25380  pi1coval  25381  elovolmr  25797  ovoliunlem3  25825  ismbf1  25945  motplusg  29005  hocsubdir  32387  hoddi  32592  lnopco0i  32606  opsqrlem1  32742  pjsdi2i  32759  pjin2i  32795  pjclem1  32797  symgfcoeu  33643  1arithidomlem1  34067  1arithidom  34069  mplvrpmfgalem  34176  mplvrpmga  34177  mplvrpmmhm  34178  mplvrpmrhm  34179  splysubrg  34192  issply  34193  eulerpartgbij  35004  cvmliftmo  36049  cvmliftlem14  36062  cvmliftiota  36066  cvmlift2lem13  36080  cvmlift2  36081  cvmliftphtlem  36082  cvmlift3lem2  36085  cvmlift3lem6  36089  cvmlift3lem7  36090  cvmlift3lem9  36092  cvmlift3  36093  msubco  36296  ftc1anclem8  38618  upixp  38663  coideq  39180  xrneq1  39328  xrneq2  39331  shiftstableeq2  39415  trlcoat  41780  trljco  41797  tgrpov  41805  tendovalco  41822  erngmul  41863  erngmul-rN  41871  dvamulr  42069  dvavadd  42072  dvhmulr  42143  dihjatcclem4  42478  rhmpsr  43611  mendmulr  44185  hoiprodcl2  47564  ovnlecvr  47567  ovncvrrp  47573  ovnsubaddlem2  47580  ovncvr2  47620  opnvonmbllem1  47641  opnvonmbl  47643  ovolval4lem2  47659  ovolval5lem2  47662  ovolval5lem3  47663  ovolval5  47664  ovnovollem2  47666  rngcinvALTV  49372  ringcinvALTV  49406  itcoval1  49774  itcoval2  49775  itcoval3  49776  itcovalsucov  49779