| 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 5867 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵)) | |
| 2 | coss2 5867 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴)) | |
| 3 | 1, 2 | anim12i 613 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴))) |
| 4 | eqss 3999 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
| 5 | eqss 3999 | . 2 ⊢ ((𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) ↔ ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴))) | |
| 6 | 3, 4, 5 | 3imtr4i 292 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ⊆ wss 3951 ∘ ccom 5689 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ss 3968 df-br 5144 df-opab 5206 df-co 5694 |
| This theorem is referenced by: coeq2i 5871 coeq2d 5873 coi2 6283 f1eqcocnv 7321 ereq1 8752 dfttrcl2 9764 seqf1olem2 14083 seqf1o 14084 relexpsucnnr 15064 isps 18613 pwsco2mhm 18846 gsumwmhm 18858 frmdgsum 18875 frmdup1 18877 frmdup2 18878 efmndov 18894 symggrplem 18897 smndex1mndlem 18922 smndex1mnd 18923 pmtr3ncom 19493 psgnunilem1 19511 frgpuplem 19790 frgpupf 19791 frgpupval 19792 gsumval3eu 19922 gsumval3lem2 19924 rngcinv 20637 ringcinv 20671 selvval 22139 rhmmpl 22387 rhmply1vr1 22391 rhmply1vsca 22392 kgencn2 23565 upxp 23631 uptx 23633 txcn 23634 xkococnlem 23667 xkococn 23668 cnmptk1 23689 cnmptkk 23691 xkofvcn 23692 imasdsf1olem 24383 pi1cof 25092 pi1coval 25093 elovolmr 25511 ovoliunlem3 25539 ismbf1 25659 motplusg 28550 hocsubdir 31804 hoddi 32009 lnopco0i 32023 opsqrlem1 32159 pjsdi2i 32176 pjin2i 32212 pjclem1 32214 symgfcoeu 33102 1arithidomlem1 33563 1arithidom 33565 eulerpartgbij 34374 cvmliftmo 35289 cvmliftlem14 35302 cvmliftiota 35306 cvmlift2lem13 35320 cvmlift2 35321 cvmliftphtlem 35322 cvmlift3lem2 35325 cvmlift3lem6 35329 cvmlift3lem7 35330 cvmlift3lem9 35332 cvmlift3 35333 msubco 35536 ftc1anclem8 37707 upixp 37736 coideq 38248 xrneq1 38378 xrneq2 38381 trlcoat 40725 trljco 40742 tgrpov 40750 tendovalco 40767 erngmul 40808 erngmul-rN 40816 dvamulr 41014 dvavadd 41017 dvhmulr 41088 dihjatcclem4 41423 rhmpsr 42562 mendmulr 43196 hoiprodcl2 46570 ovnlecvr 46573 ovncvrrp 46579 ovnsubaddlem2 46586 ovncvr2 46626 opnvonmbllem1 46647 opnvonmbl 46649 ovolval4lem2 46665 ovolval5lem2 46668 ovolval5lem3 46669 ovolval5 46670 ovnovollem2 46672 rngcinvALTV 48192 ringcinvALTV 48226 itcoval1 48584 itcoval2 48585 itcoval3 48586 itcovalsucov 48589 |
| Copyright terms: Public domain | W3C validator |