![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > coeq2 | Structured version Visualization version GIF version |
Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
Ref | Expression |
---|---|
coeq2 | ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coss2 5812 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵)) | |
2 | coss2 5812 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴)) | |
3 | 1, 2 | anim12i 613 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴))) |
4 | eqss 3959 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3959 | . 2 ⊢ ((𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) ↔ ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴))) | |
6 | 3, 4, 5 | 3imtr4i 291 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ⊆ wss 3910 ∘ ccom 5637 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3447 df-in 3917 df-ss 3927 df-br 5106 df-opab 5168 df-co 5642 |
This theorem is referenced by: coeq2i 5816 coeq2d 5818 coi2 6215 f1eqcocnv 7246 f1eqcocnvOLD 7247 ereq1 8654 dfttrcl2 9659 seqf1olem2 13947 seqf1o 13948 relexpsucnnr 14909 isps 18456 pwsco2mhm 18642 gsumwmhm 18654 frmdgsum 18671 frmdup1 18673 frmdup2 18674 efmndov 18690 symggrplem 18693 smndex1mndlem 18718 smndex1mnd 18719 pmtr3ncom 19255 psgnunilem1 19273 frgpuplem 19552 frgpupf 19553 frgpupval 19554 gsumval3eu 19679 gsumval3lem2 19681 selvval 21526 kgencn2 22906 upxp 22972 uptx 22974 txcn 22975 xkococnlem 23008 xkococn 23009 cnmptk1 23030 cnmptkk 23032 xkofvcn 23033 imasdsf1olem 23724 pi1cof 24420 pi1coval 24421 elovolmr 24838 ovoliunlem3 24866 ismbf1 24986 motplusg 27431 hocsubdir 30674 hoddi 30879 lnopco0i 30893 opsqrlem1 31029 pjsdi2i 31046 pjin2i 31082 pjclem1 31084 symgfcoeu 31877 eulerpartgbij 32912 cvmliftmo 33818 cvmliftlem14 33831 cvmliftiota 33835 cvmlift2lem13 33849 cvmlift2 33850 cvmliftphtlem 33851 cvmlift3lem2 33854 cvmlift3lem6 33858 cvmlift3lem7 33859 cvmlift3lem9 33861 cvmlift3 33862 msubco 34065 ftc1anclem8 36148 upixp 36178 coideq 36694 xrneq1 36829 xrneq2 36832 trlcoat 39176 trljco 39193 tgrpov 39201 tendovalco 39218 erngmul 39259 erngmul-rN 39267 dvamulr 39465 dvavadd 39468 dvhmulr 39539 dihjatcclem4 39874 rhmmpl 40720 mendmulr 41492 hoiprodcl2 44767 ovnlecvr 44770 ovncvrrp 44776 ovnsubaddlem2 44783 ovncvr2 44823 opnvonmbllem1 44844 opnvonmbl 44846 ovolval4lem2 44862 ovolval5lem2 44865 ovolval5lem3 44866 ovolval5 44867 ovnovollem2 44869 rngcinv 46250 rngcinvALTV 46262 ringcinv 46301 ringcinvALTV 46325 itcoval1 46720 itcoval2 46721 itcoval3 46722 itcovalsucov 46725 |
Copyright terms: Public domain | W3C validator |