![]() |
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 5862 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) | |
2 | coss1 5862 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)) | |
3 | 1, 2 | anim12i 611 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))) |
4 | eqss 3995 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3995 | . 2 ⊢ ((𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) ↔ ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))) | |
6 | 3, 4, 5 | 3imtr4i 291 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 ⊆ wss 3947 ∘ ccom 5686 |
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 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ss 3964 df-br 5154 df-opab 5216 df-co 5691 |
This theorem is referenced by: coeq1i 5866 coeq1d 5868 coi2 6274 funcoeqres 6874 wrecseq123 8329 ereq1 8741 domssex2 9175 wemapwe 9740 dfttrcl2 9767 updjud 9977 seqf1olem2 14062 seqf1o 14063 relexpsucnnl 15035 isps 18593 pwsco1mhm 18822 frmdup3 18857 efmndov 18871 symggrplem 18874 smndex1mndlem 18899 smndex1mnd 18900 pmtr3ncom 19473 psgnunilem1 19491 frgpup3 19776 gsumval3 19905 rngcinv 20615 ringcinv 20649 frgpcyg 21571 frlmup4 21799 evlseu 22098 evlsval2 22102 selvval 22130 evls1val 22311 evls1sca 22314 evl1val 22320 mpfpf1 22342 pf1mpf 22343 pf1ind 22346 xkococnlem 23654 xkococn 23655 cnmpt1k 23677 cnmptkk 23678 xkofvcn 23679 qtopeu 23711 qtophmeo 23812 utop2nei 24246 cncombf 25678 dgrcolem2 26302 dgrco 26303 motplusg 28469 hocsubdir 31718 hoddi 31923 opsqrlem1 32073 1arithidom 33412 smatfval 33610 msubco 35359 coideq 37944 trljco 40439 tgrpov 40447 tendovalco 40464 erngmul 40505 erngmul-rN 40513 cdlemksv 40543 cdlemkuu 40594 cdlemk41 40619 cdleml5N 40679 cdleml9 40683 dvamulr 40711 dvavadd 40714 dvhmulr 40785 dvhvscacbv 40797 dvhvscaval 40798 dih1dimatlem0 41027 dihjatcclem4 41120 evlsval3 42031 diophrw 42416 eldioph2 42419 diophren 42470 mendmulr 42849 fundcmpsurinjpreimafv 46980 rngcinvALTV 47653 ringcinvALTV 47687 itcoval 48049 |
Copyright terms: Public domain | W3C validator |