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 5202 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∘ ccom 5042 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-in 3547 df-ss 3554 df-br 4584 df-opab 4644 df-co 5047 |
This theorem is referenced by: coeq12i 5207 cocnvcnv2 5564 co01 5567 fcoi1 5991 dftpos2 7256 tposco 7270 canthp1 9355 cats1co 13452 isoval 16248 mvdco 17688 evlsval 19340 evl1fval1lem 19515 evl1var 19521 pf1ind 19540 imasdsf1olem 21988 hoico1 27999 hoid1i 28032 pjclem1 28438 pjclem3 28440 pjci 28443 dfpo2 30898 poimirlem9 32588 cdlemk45 35253 cononrel1 36919 trclubgNEW 36944 trclrelexplem 37022 relexpaddss 37029 cotrcltrcl 37036 cortrcltrcl 37051 corclrtrcl 37052 cotrclrcl 37053 cortrclrcl 37054 cotrclrtrcl 37055 cortrclrtrcl 37056 brco3f1o 37351 clsneibex 37420 neicvgbex 37430 subsaliuncl 39252 meadjiun 39359 |
Copyright terms: Public domain | W3C validator |