Theorem coeq2i 5862

Description: Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)

Hypothesis

Ref	Expression
coeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
coeq2i	⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)

Proof of Theorem coeq2i

Step	Hyp	Ref	Expression
1		coeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		coeq2 5860	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)

Syntax hints:   = wceq 1533   ∘ ccom 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ss 3962  df-br 5149  df-opab 5211  df-co 5686

This theorem is referenced by:  coeq12i  5865  cocnvcnv2  6262  co01  6265  dfpo2  6300  fcoi1  6769  f1ofvswap  7312  dftpos2  8247  tposco  8261  cottrcl  9742  canthp1  10677  cats1co  14839  isoval  17747  mvdco  19404  evlsval  22039  evl1fval1lem  22258  evl1var  22264  pf1ind  22283  rhmply1vr1  22317  rhmply1vsca  22318  imasdsf1olem  24309  hoico1  31622  hoid1i  31655  pjclem1  32061  pjclem3  32063  pjci  32066  cycpmconjv  32920  cycpmconjs  32934  poimirlem9  37172  cdlemk45  40489  cononrel1  43089  trclubgNEW  43113  trclrelexplem  43206  relexpaddss  43213  cotrcltrcl  43220  cortrcltrcl  43235  corclrtrcl  43236  cotrclrcl  43237  cortrclrcl  43238  cotrclrtrcl  43239  cortrclrtrcl  43240  brco3f1o  43528  clsneibex  43597  neicvgbex  43607  subsaliuncl  45809  meadjiun  45917  fundcmpsurinjimaid  46814

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »