| 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 5868 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∘ ccom 5689 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ss 3968 df-br 5144 df-opab 5206 df-co 5694 |
| This theorem is referenced by: coeq12i 5874 cocnvcnv1 6277 ttrclco 9758 hashgval 14372 imasdsval2 17561 prds1 20320 pf1mpf 22356 upxp 23631 uptx 23633 hoico2 31776 hoid1ri 31809 nmopcoadj2i 32121 pjclem3 32216 cycpmconjslem1 33174 cycpmconjs 33176 cyc3conja 33177 1arithidomlem2 33564 erdsze2lem2 35209 pprodcnveq 35884 diblss 41172 cononrel2 43608 trclubgNEW 43631 cortrcltrcl 43753 corclrtrcl 43754 cortrclrcl 43756 cotrclrtrcl 43757 cortrclrtrcl 43758 neicvgbex 44125 neicvgnvo 44128 dvsinax 45928 |
| Copyright terms: Public domain | W3C validator |