![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > coeq1d | Structured version Visualization version GIF version |
Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
Ref | Expression |
---|---|
coeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
coeq1d | ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coeq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | coeq1 5312 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = 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: coeq12d 5319 fcof1oinvd 6588 domss2 8160 mapen 8165 mapfien 8354 hashfacen 13276 relexpsucnnr 13809 relexpsucr 13813 relexpsucnnl 13816 relexpaddnn 13835 imasval 16218 cofuass 16596 cofulid 16597 setcinv 16787 catcisolem 16803 catciso 16804 yonedalem3b 16966 gsumvalx 17317 frmdup3lem 17450 symggrp 17866 f1omvdco2 17914 symggen 17936 psgnunilem1 17959 gsumval3 18354 gsumzf1o 18359 psrass1lem 19425 coe1add 19682 evls1fval 19732 evl1sca 19746 evl1var 19748 evls1var 19750 pf1mpf 19764 pf1ind 19767 znval 19931 znle2 19950 tchds 23076 dvnfval 23730 hocsubdir 28772 fcoinver 29544 fcobij 29628 symgfcoeu 29973 reprpmtf1o 30832 hgt750lemg 30860 subfacp1lem5 31292 mrsubffval 31530 mrsubfval 31531 mrsubrn 31536 elmrsubrn 31543 upixp 33654 ltrncoidN 35732 trlcoat 36328 trlcone 36333 cdlemg47a 36339 cdlemg47 36341 ltrnco4 36344 tendovalco 36370 tendoplcbv 36380 tendopl 36381 tendoplass 36388 tendo0pl 36396 tendoipl 36402 cdlemk45 36552 cdlemk53b 36561 cdlemk55a 36564 erngdvlem3 36595 erngdvlem3-rN 36603 tendocnv 36627 dvhvaddcbv 36695 dvhvaddval 36696 dvhvaddass 36703 dicvscacl 36797 cdlemn8 36810 dihordlem7b 36821 dihopelvalcpre 36854 relexp2 38286 relexpxpnnidm 38312 relexpiidm 38313 relexpmulnn 38318 relexpaddss 38327 trclfvcom 38332 trclfvdecomr 38337 frege131d 38373 dssmap2d 38633 |
Copyright terms: Public domain | W3C validator |