![]() |
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 5615 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 ∘ ccom 5447 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-in 3866 df-ss 3874 df-br 4963 df-opab 5025 df-co 5452 |
This theorem is referenced by: coeq12i 5620 cocnvcnv2 5986 co01 5989 fcoi1 6420 dftpos2 7760 tposco 7774 canthp1 9922 cats1co 14054 isoval 16864 mvdco 18304 evlsval 19986 evl1fval1lem 20175 evl1var 20181 pf1ind 20200 imasdsf1olem 22666 hoico1 29224 hoid1i 29257 pjclem1 29663 pjclem3 29665 pjci 29668 cycpmconjv 30421 cycpmconjs 30436 dfpo2 32599 poimirlem9 34432 cdlemk45 37614 cononrel1 39439 trclubgNEW 39463 trclrelexplem 39541 relexpaddss 39548 cotrcltrcl 39555 cortrcltrcl 39570 corclrtrcl 39571 cotrclrcl 39572 cortrclrcl 39573 cotrclrtrcl 39574 cortrclrtrcl 39575 brco3f1o 39868 clsneibex 39937 neicvgbex 39947 subsaliuncl 42183 meadjiun 42290 |
Copyright terms: Public domain | W3C validator |