![]() |
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 5814 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∘ ccom 5637 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3447 df-in 3917 df-ss 3927 df-br 5106 df-opab 5168 df-co 5642 |
This theorem is referenced by: coeq12i 5819 cocnvcnv2 6210 co01 6213 dfpo2 6248 fcoi1 6716 f1ofvswap 7251 dftpos2 8173 tposco 8187 cottrcl 9654 canthp1 10589 cats1co 14744 isoval 17647 mvdco 19225 evlsval 21494 evl1fval1lem 21694 evl1var 21700 pf1ind 21719 imasdsf1olem 23724 hoico1 30645 hoid1i 30678 pjclem1 31084 pjclem3 31086 pjci 31089 cycpmconjv 31935 cycpmconjs 31949 poimirlem9 36077 cdlemk45 39400 cononrel1 41847 trclubgNEW 41871 trclrelexplem 41964 relexpaddss 41971 cotrcltrcl 41978 cortrcltrcl 41993 corclrtrcl 41994 cotrclrcl 41995 cortrclrcl 41996 cotrclrtrcl 41997 cortrclrtrcl 41998 brco3f1o 42286 clsneibex 42355 neicvgbex 42365 subsaliuncl 44570 meadjiun 44678 fundcmpsurinjimaid 45574 |
Copyright terms: Public domain | W3C validator |