| 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 6045 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1560 “ cima 5650 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-ext 2734 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-sb 2091 df-clab 2741 df-cleq 2754 df-clel 2837 df-rab 3415 df-v 3456 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4481 df-sn 4583 df-pr 4585 df-op 4589 df-br 5101 df-opab 5163 df-xp 5653 df-cnv 5655 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 |
| This theorem is referenced by: cnvimarndm 6072 dmco 6242 imain 6606 fnimapr 6950 fnimatpd 6951 ssimaex 6952 intpreima 7051 resfunexg 7199 imauni 7230 isoini2 7323 fsuppeq 8155 fsuppeqg 8156 naddasslem1 8665 naddasslem2 8666 uniqs 8755 pwfilem 9262 fiint 9271 jech9.3 9772 infxpenlem 9969 hsmexlem4 10386 fcdmnn0supp 12538 fcdmnn0fsupp 12539 fcdmnn0suppg 12540 hashkf 14345 ghmeqker 19283 gsumval3lem1 19945 gsumval3lem2 19946 islinds2 21865 lindsind2 21871 mhpmulcl 22214 snclseqg 24176 retopbas 24820 ismbf3d 25716 i1fima 25740 i1fd 25743 itg1addlem5 25762 limciun 25956 plyeq0 26271 bday0 27904 bday1 27907 madeval2 27926 old1 27958 madeoldsuc 27978 bdayiun 28008 neg0s 28119 neg1s 28120 negbdaylem 28149 oncutlt 28357 oniso 28364 bdayons 28369 n0bday 28445 bdayn0p1 28462 spthispth 29924 0pth 30327 1pthdlem2 30338 eupth2lemb 30439 htth 31121 fcoinver 32804 ffs2 32929 ffsrn 32930 tocyccntz 33324 elrspunidl 33614 sibfof 34637 eulerpartgbij 34669 eulerpartlemmf 34672 eulerpartlemgh 34675 eulerpart 34679 fiblem 34695 orrvcval4 34762 cvmsss2 35624 opelco3 36125 poimirlem3 38122 poimirlem30 38149 mbfposadd 38166 itg2addnclem2 38171 ftc1anclem5 38196 ftc1anclem6 38197 pwfi2f1o 43673 brtrclfv2 44303 binomcxp 44933 fcoreslem1 47657 isubgr3stgrlem6 48593 |
| Copyright terms: Public domain | W3C validator |