| 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 5866 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) | |
| 2 | coss1 5866 | . . 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: coeq1i 5870 coeq1d 5872 coi2 6283 funcoeqres 6879 wrecseq123 8339 ereq1 8752 domssex2 9177 wemapwe 9737 dfttrcl2 9764 updjud 9974 seqf1olem2 14083 seqf1o 14084 relexpsucnnl 15069 isps 18613 pwsco1mhm 18845 frmdup3 18880 efmndov 18894 symggrplem 18897 smndex1mndlem 18922 smndex1mnd 18923 pmtr3ncom 19493 psgnunilem1 19511 frgpup3 19796 gsumval3 19925 rngcinv 20637 ringcinv 20671 frgpcyg 21592 frlmup4 21821 evlseu 22107 evlsval2 22111 selvval 22139 evls1val 22324 evls1sca 22327 evl1val 22333 mpfpf1 22355 pf1mpf 22356 pf1ind 22359 xkococnlem 23667 xkococn 23668 cnmpt1k 23690 cnmptkk 23691 xkofvcn 23692 qtopeu 23724 qtophmeo 23825 utop2nei 24259 cncombf 25693 dgrcolem2 26314 dgrco 26315 motplusg 28550 hocsubdir 31804 hoddi 32009 opsqrlem1 32159 1arithidom 33565 smatfval 33794 msubco 35536 coideq 38248 trljco 40742 tgrpov 40750 tendovalco 40767 erngmul 40808 erngmul-rN 40816 cdlemksv 40846 cdlemkuu 40897 cdlemk41 40922 cdleml5N 40982 cdleml9 40986 dvamulr 41014 dvavadd 41017 dvhmulr 41088 dvhvscacbv 41100 dvhvscaval 41101 dih1dimatlem0 41330 dihjatcclem4 41423 evlsval3 42569 diophrw 42770 eldioph2 42773 diophren 42824 mendmulr 43196 fundcmpsurinjpreimafv 47395 rngcinvALTV 48192 ringcinvALTV 48226 itcoval 48582 |
| Copyright terms: Public domain | W3C validator |