| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > imaeq2i | Structured version Visualization version GIF version | ||
| Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.) |
| Ref | Expression |
|---|---|
| imaeq1i.1 | ⊢ 𝐴 = 𝐵 |
| Ref | Expression |
|---|---|
| imaeq2i | ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imaeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
| 2 | imaeq2 6074 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 “ 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-xp 5691 df-cnv 5693 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 |
| This theorem is referenced by: cnvimarndm 6101 dmco 6274 imain 6651 fnimapr 6992 fnimatpd 6993 ssimaex 6994 intpreima 7090 resfunexg 7235 imauni 7266 isoini2 7359 fsuppeq 8200 fsuppeqg 8201 naddasslem1 8732 naddasslem2 8733 uniqs 8817 pwfilem 9356 fiint 9366 fiintOLD 9367 jech9.3 9854 infxpenlem 10053 hsmexlem4 10469 fcdmnn0supp 12583 fcdmnn0fsupp 12584 fcdmnn0suppg 12585 hashkf 14371 ghmeqker 19261 gsumval3lem1 19923 gsumval3lem2 19924 islinds2 21833 lindsind2 21839 mhpmulcl 22153 snclseqg 24124 retopbas 24781 ismbf3d 25689 i1fima 25713 i1fd 25716 itg1addlem5 25735 limciun 25929 plyeq0 26250 bday0s 27873 bday1s 27876 madeval2 27892 old1 27914 madeoldsuc 27923 negs0s 28058 negs1s 28059 negsbdaylem 28088 n0sbday 28354 spthispth 29744 0pth 30144 1pthdlem2 30155 eupth2lemb 30256 htth 30937 fcoinver 32617 ffs2 32739 ffsrn 32740 tocyccntz 33164 elrspunidl 33456 sibfof 34342 eulerpartgbij 34374 eulerpartlemmf 34377 eulerpartlemgh 34380 eulerpart 34384 fiblem 34400 orrvcval4 34467 cvmsss2 35279 opelco3 35775 poimirlem3 37630 poimirlem30 37657 mbfposadd 37674 itg2addnclem2 37679 ftc1anclem5 37704 ftc1anclem6 37705 uniqsALTV 38330 pwfi2f1o 43108 brtrclfv2 43740 binomcxp 44376 fcoreslem1 47075 isubgr3stgrlem6 47938 |
| Copyright terms: Public domain | W3C validator |