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 5277 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) | |
2 | coss1 5277 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)) | |
3 | 1, 2 | anim12i 590 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))) |
4 | eqss 3618 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3618 | . 2 ⊢ ((𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) ↔ ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))) | |
6 | 3, 4, 5 | 3imtr4i 281 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ⊆ wss 3574 ∘ ccom 5118 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-in 3581 df-ss 3588 df-br 4654 df-opab 4713 df-co 5123 |
This theorem is referenced by: coeq1i 5281 coeq1d 5283 coi2 5652 relcnvtr 5655 funcoeqres 6167 ereq1 7749 domssex2 8120 wemapwe 8594 seqf1olem2 12841 seqf1o 12842 relexpsucnnl 13772 isps 17202 pwsco1mhm 17370 frmdup3 17404 symgov 17810 pmtr3ncom 17895 psgnunilem1 17913 frgpup3 18191 gsumval3 18308 evlseu 19516 evlsval2 19520 evls1val 19685 evls1sca 19688 evl1val 19693 mpfpf1 19715 pf1mpf 19716 pf1ind 19719 frgpcyg 19922 frlmup4 20140 xkococnlem 21462 xkococn 21463 cnmpt1k 21485 cnmptkk 21486 xkofvcn 21487 qtopeu 21519 qtophmeo 21620 utop2nei 22054 cncombf 23425 dgrcolem2 24030 dgrco 24031 motplusg 25437 hocsubdir 28644 hoddi 28849 opsqrlem1 28999 smatfval 29861 msubco 31428 coideq 34009 trljco 36028 tgrpov 36036 tendovalco 36053 erngmul 36094 erngmul-rN 36102 cdlemksv 36132 cdlemkuu 36183 cdlemk41 36208 cdleml5N 36268 cdleml9 36272 dvamulr 36300 dvavadd 36303 dvhmulr 36375 dvhvscacbv 36387 dvhvscaval 36388 dih1dimatlem0 36617 dihjatcclem4 36710 diophrw 37322 eldioph2 37325 diophren 37377 mendmulr 37758 rngcinv 41981 rngcinvALTV 41993 ringcinv 42032 ringcinvALTV 42056 |
Copyright terms: Public domain | W3C validator |