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 5721 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1531 ∘ ccom 5552 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-in 3941 df-ss 3950 df-br 5058 df-opab 5120 df-co 5557 |
This theorem is referenced by: coeq12i 5727 cocnvcnv1 6103 hashgval 13685 imasdsval2 16781 prds1 19356 pf1mpf 20507 upxp 22223 uptx 22225 hoico2 29526 hoid1ri 29559 nmopcoadj2i 29871 pjclem3 29966 cycpmconjslem1 30789 cycpmconjs 30791 cyc3conja 30792 erdsze2lem2 32444 pprodcnveq 33337 diblss 38298 cononrel2 39946 trclubgNEW 39969 cortrcltrcl 40076 corclrtrcl 40077 cortrclrcl 40079 cotrclrtrcl 40080 cortrclrtrcl 40081 neicvgbex 40453 neicvgnvo 40456 dvsinax 42187 |
Copyright terms: Public domain | W3C validator |