![]() |
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 5312 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ∘ ccom 5147 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-in 3614 df-ss 3621 df-br 4686 df-opab 4746 df-co 5152 |
This theorem is referenced by: coeq12i 5318 cocnvcnv1 5684 hashgval 13160 imasdsval2 16223 prds1 18660 pf1mpf 19764 upxp 21474 uptx 21476 hoico2 28744 hoid1ri 28777 nmopcoadj2i 29089 pjclem3 29184 erdsze2lem2 31312 pprodcnveq 32115 diblss 36776 cononrel2 38218 trclubgNEW 38242 cortrcltrcl 38349 corclrtrcl 38350 cortrclrcl 38352 cotrclrtrcl 38353 cortrclrtrcl 38354 neicvgbex 38727 neicvgnvo 38730 dvsinax 40445 |
Copyright terms: Public domain | W3C validator |