![]() |
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 5974 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) | |
2 | 1 | rneqd 5936 | . 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶)) |
3 | df-ima 5689 | . 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶) | |
4 | df-ima 5689 | . 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶) | |
5 | 2, 3, 4 | 3eqtr4g 2798 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ran crn 5677 ↾ cres 5678 “ cima 5679 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-cnv 5684 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 |
This theorem is referenced by: imaeq1i 6055 imaeq1d 6057 suppval 8145 naddcllem 8672 eceq2 8740 marypha1lem 9425 marypha1 9426 ackbij2lem2 10232 ackbij2lem3 10233 r1om 10236 limsupval 15415 isacs1i 17598 mreacs 17599 islindf 21359 iscnp 22733 xkoccn 23115 xkohaus 23149 xkoco1cn 23153 xkoco2cn 23154 xkococnlem 23155 xkococn 23156 xkoinjcn 23183 fmval 23439 fmf 23441 utoptop 23731 restutop 23734 restutopopn 23735 ustuqtoplem 23736 ustuqtop1 23738 ustuqtop2 23739 ustuqtop4 23741 ustuqtop5 23742 utopsnneiplem 23744 utopsnnei 23746 neipcfilu 23793 psmetutop 24068 cfilfval 24773 elply2 25702 coeeu 25731 coelem 25732 coeeq 25733 dmarea 26452 negsval 27490 mclsax 34549 tailfval 35246 bj-cleq 35832 bj-funun 36122 poimirlem15 36492 poimirlem24 36501 brtrclfv2 42464 liminfval 44462 isomgreqve 46480 isomgrsym 46491 isomgrtr 46494 ushrisomgr 46496 |
Copyright terms: Public domain | W3C validator |