| 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 5991 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) | |
| 2 | 1 | rneqd 5949 | . 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶)) |
| 3 | df-ima 5698 | . 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶) | |
| 4 | df-ima 5698 | . 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶) | |
| 5 | 2, 3, 4 | 3eqtr4g 2802 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ran crn 5686 ↾ cres 5687 “ cima 5688 |
| 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-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-cnv 5693 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 |
| This theorem is referenced by: imaeq1i 6075 imaeq1d 6077 suppval 8187 naddcllem 8714 eceq2 8786 marypha1lem 9473 marypha1 9474 ackbij2lem2 10279 ackbij2lem3 10280 r1om 10283 limsupval 15510 isacs1i 17700 mreacs 17701 islindf 21832 iscnp 23245 xkoccn 23627 xkohaus 23661 xkoco1cn 23665 xkoco2cn 23666 xkococnlem 23667 xkococn 23668 xkoinjcn 23695 fmval 23951 fmf 23953 utoptop 24243 restutop 24246 restutopopn 24247 ustuqtoplem 24248 ustuqtop1 24250 ustuqtop2 24251 ustuqtop4 24253 ustuqtop5 24254 utopsnneiplem 24256 utopsnnei 24258 neipcfilu 24305 psmetutop 24580 cfilfval 25298 elply2 26235 coeeu 26264 coelem 26265 coeeq 26266 dmarea 27000 negsval 28057 mclsax 35574 tailfval 36373 bj-cleq 36963 bj-funun 37253 poimirlem15 37642 poimirlem24 37651 brtrclfv2 43740 liminfval 45774 ushggricedg 47896 uhgrimisgrgric 47899 |
| Copyright terms: Public domain | W3C validator |