![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > coeq1 | Structured version Visualization version GIF version |
Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
Ref | Expression |
---|---|
coeq1 | ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coss1 5812 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) | |
2 | coss1 5812 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)) | |
3 | 1, 2 | anim12i 614 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))) |
4 | eqss 3960 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3960 | . 2 ⊢ ((𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) ↔ ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))) | |
6 | 3, 4, 5 | 3imtr4i 292 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ⊆ wss 3911 ∘ ccom 5638 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3446 df-in 3918 df-ss 3928 df-br 5107 df-opab 5169 df-co 5643 |
This theorem is referenced by: coeq1i 5816 coeq1d 5818 coi2 6216 funcoeqres 6816 wrecseq123 8246 ereq1 8658 domssex2 9084 wemapwe 9638 dfttrcl2 9665 updjud 9875 seqf1olem2 13954 seqf1o 13955 relexpsucnnl 14921 isps 18462 pwsco1mhm 18647 frmdup3 18682 efmndov 18696 symggrplem 18699 smndex1mndlem 18724 smndex1mnd 18725 pmtr3ncom 19262 psgnunilem1 19280 frgpup3 19565 gsumval3 19689 frgpcyg 20996 frlmup4 21223 evlseu 21509 evlsval2 21513 selvval 21544 evls1val 21702 evls1sca 21705 evl1val 21711 mpfpf1 21733 pf1mpf 21734 pf1ind 21737 xkococnlem 23026 xkococn 23027 cnmpt1k 23049 cnmptkk 23050 xkofvcn 23051 qtopeu 23083 qtophmeo 23184 utop2nei 23618 cncombf 25038 dgrcolem2 25651 dgrco 25652 motplusg 27526 hocsubdir 30769 hoddi 30974 opsqrlem1 31124 smatfval 32433 msubco 34182 coideq 36750 trljco 39249 tgrpov 39257 tendovalco 39274 erngmul 39315 erngmul-rN 39323 cdlemksv 39353 cdlemkuu 39404 cdlemk41 39429 cdleml5N 39489 cdleml9 39493 dvamulr 39521 dvavadd 39524 dvhmulr 39595 dvhvscacbv 39607 dvhvscaval 39608 dih1dimatlem0 39837 dihjatcclem4 39930 evlsval3 40787 diophrw 41125 eldioph2 41128 diophren 41179 mendmulr 41558 fundcmpsurinjpreimafv 45686 rngcinv 46365 rngcinvALTV 46377 ringcinv 46416 ringcinvALTV 46440 itcoval 46833 |
Copyright terms: Public domain | W3C validator |