![]() |
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 5511 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) | |
2 | coss1 5511 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)) | |
3 | 1, 2 | anim12i 608 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))) |
4 | eqss 3843 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3843 | . 2 ⊢ ((𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) ↔ ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))) | |
6 | 3, 4, 5 | 3imtr4i 284 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1658 ⊆ wss 3799 ∘ ccom 5347 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-in 3806 df-ss 3813 df-br 4875 df-opab 4937 df-co 5352 |
This theorem is referenced by: coeq1i 5515 coeq1d 5517 coi2 5894 relcnvtr 5897 funcoeqres 6409 ereq1 8017 domssex2 8390 wemapwe 8872 updjud 9074 seqf1olem2 13136 seqf1o 13137 relexpsucnnl 14150 isps 17556 pwsco1mhm 17724 frmdup3 17759 symgov 18161 pmtr3ncom 18246 psgnunilem1 18264 frgpup3 18545 gsumval3 18662 evlseu 19877 evlsval2 19881 evls1val 20046 evls1sca 20049 evl1val 20054 mpfpf1 20076 pf1mpf 20077 pf1ind 20080 frgpcyg 20282 frlmup4 20508 xkococnlem 21834 xkococn 21835 cnmpt1k 21857 cnmptkk 21858 xkofvcn 21859 qtopeu 21891 qtophmeo 21992 utop2nei 22425 cncombf 23825 dgrcolem2 24430 dgrco 24431 motplusg 25855 hocsubdir 29200 hoddi 29405 opsqrlem1 29555 smatfval 30407 msubco 31975 coideq 34565 trljco 36816 tgrpov 36824 tendovalco 36841 erngmul 36882 erngmul-rN 36890 cdlemksv 36920 cdlemkuu 36971 cdlemk41 36996 cdleml5N 37056 cdleml9 37060 dvamulr 37088 dvavadd 37091 dvhmulr 37162 dvhvscacbv 37174 dvhvscaval 37175 dih1dimatlem0 37404 dihjatcclem4 37497 diophrw 38167 eldioph2 38170 diophren 38222 mendmulr 38602 rngcinv 42829 rngcinvALTV 42841 ringcinv 42880 ringcinvALTV 42904 |
Copyright terms: Public domain | W3C validator |