![]() |
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 5528 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) | |
2 | 1 | rneqd 5491 | . 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶)) |
3 | df-ima 5262 | . 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶) | |
4 | df-ima 5262 | . 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶) | |
5 | 2, 3, 4 | 3eqtr4g 2830 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1631 ran crn 5250 ↾ cres 5251 “ cima 5252 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-rab 3070 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-sn 4317 df-pr 4319 df-op 4323 df-br 4787 df-opab 4847 df-cnv 5257 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 |
This theorem is referenced by: imaeq1i 5604 imaeq1d 5606 suppval 7448 eceq2 7936 marypha1lem 8495 marypha1 8496 ackbij2lem2 9264 ackbij2lem3 9265 r1om 9268 limsupval 14413 isacs1i 16525 mreacs 16526 islindf 20368 iscnp 21262 xkoccn 21643 xkohaus 21677 xkoco1cn 21681 xkoco2cn 21682 xkococnlem 21683 xkococn 21684 xkoinjcn 21711 fmval 21967 fmf 21969 utoptop 22258 restutop 22261 restutopopn 22262 ustuqtoplem 22263 ustuqtop1 22265 ustuqtop2 22266 ustuqtop4 22268 ustuqtop5 22269 utopsnneiplem 22271 utopsnnei 22273 neipcfilu 22320 psmetutop 22592 cfilfval 23281 elply2 24172 coeeu 24201 coelem 24202 coeeq 24203 dmarea 24905 mclsax 31804 tailfval 32704 bj-cleq 33280 poimirlem15 33757 poimirlem24 33766 brtrclfv2 38545 liminfval 40509 |
Copyright terms: Public domain | W3C validator |