Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > coeq1i | 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 |
---|---|
coeq1i | ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | coeq1 5727 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∘ ccom 5558 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-in 3942 df-ss 3951 df-br 5066 df-opab 5128 df-co 5563 |
This theorem is referenced by: coeq12i 5733 cocnvcnv1 6109 hashgval 13692 imasdsval2 16788 prds1 19363 pf1mpf 20514 upxp 22230 uptx 22232 hoico2 29533 hoid1ri 29566 nmopcoadj2i 29878 pjclem3 29973 cycpmconjslem1 30796 cycpmconjs 30798 cyc3conja 30799 erdsze2lem2 32451 pprodcnveq 33344 diblss 38305 cononrel2 39953 trclubgNEW 39976 cortrcltrcl 40083 corclrtrcl 40084 cortrclrcl 40086 cotrclrtrcl 40087 cortrclrtrcl 40088 neicvgbex 40460 neicvgnvo 40463 dvsinax 42195 |
Copyright terms: Public domain | W3C validator |