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 5720 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) | |
2 | coss1 5720 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)) | |
3 | 1, 2 | anim12i 614 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))) |
4 | eqss 3981 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3981 | . 2 ⊢ ((𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) ↔ ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))) | |
6 | 3, 4, 5 | 3imtr4i 294 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1533 ⊆ wss 3935 ∘ ccom 5553 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-in 3942 df-ss 3951 df-br 5059 df-opab 5121 df-co 5558 |
This theorem is referenced by: coeq1i 5724 coeq1d 5726 coi2 6110 funcoeqres 6639 ereq1 8290 domssex2 8671 wemapwe 9154 updjud 9357 seqf1olem2 13404 seqf1o 13405 relexpsucnnl 14385 isps 17806 pwsco1mhm 17990 frmdup3 18026 efmndov 18040 symggrplem 18043 smndex1mndlem 18068 smndex1mnd 18069 pmtr3ncom 18597 psgnunilem1 18615 frgpup3 18898 gsumval3 19021 evlseu 20290 evlsval2 20294 selvval 20325 evls1val 20477 evls1sca 20480 evl1val 20486 mpfpf1 20508 pf1mpf 20509 pf1ind 20512 frgpcyg 20714 frlmup4 20939 xkococnlem 22261 xkococn 22262 cnmpt1k 22284 cnmptkk 22285 xkofvcn 22286 qtopeu 22318 qtophmeo 22419 utop2nei 22853 cncombf 24253 dgrcolem2 24858 dgrco 24859 motplusg 26322 hocsubdir 29556 hoddi 29761 opsqrlem1 29911 smatfval 31055 msubco 32773 coideq 35501 trljco 37870 tgrpov 37878 tendovalco 37895 erngmul 37936 erngmul-rN 37944 cdlemksv 37974 cdlemkuu 38025 cdlemk41 38050 cdleml5N 38110 cdleml9 38114 dvamulr 38142 dvavadd 38145 dvhmulr 38216 dvhvscacbv 38228 dvhvscaval 38229 dih1dimatlem0 38458 dihjatcclem4 38551 diophrw 39349 eldioph2 39352 diophren 39403 mendmulr 39781 fundcmpsurinjpreimafv 43562 rngcinv 44246 rngcinvALTV 44258 ringcinv 44297 ringcinvALTV 44321 |
Copyright terms: Public domain | W3C validator |