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 5840 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) | |
2 | 1 | rneqd 5801 | . 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶)) |
3 | df-ima 5561 | . 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶) | |
4 | df-ima 5561 | . 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶) | |
5 | 2, 3, 4 | 3eqtr4g 2878 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ran crn 5549 ↾ cres 5550 “ cima 5551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-opab 5120 df-cnv 5556 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 |
This theorem is referenced by: imaeq1i 5919 imaeq1d 5921 suppval 7821 eceq2 8318 marypha1lem 8885 marypha1 8886 ackbij2lem2 9650 ackbij2lem3 9651 r1om 9654 limsupval 14819 isacs1i 16916 mreacs 16917 islindf 20884 iscnp 21773 xkoccn 22155 xkohaus 22189 xkoco1cn 22193 xkoco2cn 22194 xkococnlem 22195 xkococn 22196 xkoinjcn 22223 fmval 22479 fmf 22481 utoptop 22770 restutop 22773 restutopopn 22774 ustuqtoplem 22775 ustuqtop1 22777 ustuqtop2 22778 ustuqtop4 22780 ustuqtop5 22781 utopsnneiplem 22783 utopsnnei 22785 neipcfilu 22832 psmetutop 23104 cfilfval 23794 elply2 24713 coeeu 24742 coelem 24743 coeeq 24744 dmarea 25462 mclsax 32713 tailfval 33617 bj-cleq 34171 bj-funun 34426 poimirlem15 34788 poimirlem24 34797 brtrclfv2 39950 liminfval 41916 isomgreqve 43867 isomgrsym 43878 isomgrtr 43881 ushrisomgr 43883 |
Copyright terms: Public domain | W3C validator |