![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > coeq2i | Structured version Visualization version GIF version |
Description: Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
Ref | Expression |
---|---|
coeq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
coeq2i | ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | coeq2 5865 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∘ ccom 5686 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ss 3964 df-br 5154 df-opab 5216 df-co 5691 |
This theorem is referenced by: coeq12i 5870 cocnvcnv2 6269 co01 6272 dfpo2 6307 fcoi1 6776 f1ofvswap 7319 dftpos2 8258 tposco 8272 cottrcl 9762 canthp1 10697 cats1co 14865 isoval 17781 mvdco 19443 evlsval 22101 evl1fval1lem 22321 evl1var 22327 pf1ind 22346 rhmply1vr1 22378 rhmply1vsca 22379 imasdsf1olem 24370 hoico1 31689 hoid1i 31722 pjclem1 32128 pjclem3 32130 pjci 32133 cycpmconjv 33020 cycpmconjs 33034 poimirlem9 37330 cdlemk45 40646 cononrel1 43261 trclubgNEW 43285 trclrelexplem 43378 relexpaddss 43385 cotrcltrcl 43392 cortrcltrcl 43407 corclrtrcl 43408 cotrclrcl 43409 cortrclrcl 43410 cotrclrtrcl 43411 cortrclrtrcl 43412 brco3f1o 43700 clsneibex 43769 neicvgbex 43779 subsaliuncl 45979 meadjiun 46087 fundcmpsurinjimaid 46983 |
Copyright terms: Public domain | W3C validator |