![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imaeq1 | Structured version Visualization version GIF version |
Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
imaeq1 | ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reseq1 5592 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) | |
2 | 1 | rneqd 5554 | . 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶)) |
3 | df-ima 5323 | . 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶) | |
4 | df-ima 5323 | . 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶) | |
5 | 2, 3, 4 | 3eqtr4g 2856 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 ran crn 5311 ↾ cres 5312 “ cima 5313 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-rab 3096 df-v 3385 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-sn 4367 df-pr 4369 df-op 4373 df-br 4842 df-opab 4904 df-cnv 5318 df-dm 5320 df-rn 5321 df-res 5322 df-ima 5323 |
This theorem is referenced by: imaeq1i 5678 imaeq1d 5680 suppval 7532 eceq2 8020 marypha1lem 8579 marypha1 8580 ackbij2lem2 9348 ackbij2lem3 9349 r1om 9352 limsupval 14543 isacs1i 16629 mreacs 16630 islindf 20473 iscnp 21367 xkoccn 21748 xkohaus 21782 xkoco1cn 21786 xkoco2cn 21787 xkococnlem 21788 xkococn 21789 xkoinjcn 21816 fmval 22072 fmf 22074 utoptop 22363 restutop 22366 restutopopn 22367 ustuqtoplem 22368 ustuqtop1 22370 ustuqtop2 22371 ustuqtop4 22373 ustuqtop5 22374 utopsnneiplem 22376 utopsnnei 22378 neipcfilu 22425 psmetutop 22697 cfilfval 23387 elply2 24290 coeeu 24319 coelem 24320 coeeq 24321 dmarea 25033 mclsax 31975 tailfval 32871 bj-cleq 33433 poimirlem15 33905 poimirlem24 33914 brtrclfv2 38790 liminfval 40723 isomgreqve 42483 isomgrsym 42494 isomgrtr 42497 ushrisomgr 42499 |
Copyright terms: Public domain | W3C validator |