![]() |
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 6055 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1540 “ cima 5679 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 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-xp 5682 df-cnv 5684 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 |
This theorem is referenced by: cnvimarndm 6081 dmco 6253 imain 6633 fnimapr 6975 ssimaex 6976 intpreima 7071 resfunexg 7219 imauni 7248 isoini2 7339 fsuppeq 8165 fsuppeqg 8166 naddasslem1 8699 naddasslem2 8700 uniqs 8777 pwfilem 9183 fiint 9330 jech9.3 9815 infxpenlem 10014 hsmexlem4 10430 fcdmnn0supp 12535 fcdmnn0fsupp 12536 fcdmnn0suppg 12537 hashkf 14299 ghmeqker 19164 gsumval3lem1 19821 gsumval3lem2 19822 islinds2 21679 lindsind2 21685 mhpmulcl 22002 snclseqg 23941 retopbas 24598 ismbf3d 25504 i1fima 25528 i1fd 25531 itg1addlem5 25551 limciun 25744 plyeq0 26064 bday0s 27676 bday1s 27679 madeval2 27695 old1 27717 madeoldsuc 27726 negs0s 27854 negsbdaylem 27883 spthispth 29418 0pth 29813 1pthdlem2 29824 eupth2lemb 29925 htth 30606 fcoinver 32270 fnimatp 32337 ffs2 32388 ffsrn 32389 tocyccntz 32741 elrspunidl 32988 sibfof 33805 eulerpartgbij 33837 eulerpartlemmf 33840 eulerpartlemgh 33843 eulerpart 33847 fiblem 33863 orrvcval4 33929 cvmsss2 34731 opelco3 35218 poimirlem3 36958 poimirlem30 36985 mbfposadd 37002 itg2addnclem2 37007 ftc1anclem5 37032 ftc1anclem6 37033 uniqsALTV 37665 pwfi2f1o 42304 brtrclfv2 42944 binomcxp 43582 fcoreslem1 46235 |
Copyright terms: Public domain | W3C validator |