| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > imaeq1i | Structured version Visualization version GIF version | ||
| Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.) |
| Ref | Expression |
|---|---|
| imaeq1i.1 | ⊢ 𝐴 = 𝐵 |
| Ref | Expression |
|---|---|
| imaeq1i | ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imaeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
| 2 | imaeq1 6073 | . 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-cnv 5693 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 |
| This theorem is referenced by: mptpreima 6258 csbpredg 6327 isarep2 6658 suppun 8209 suppco 8231 fsuppun 9427 fsuppcolem 9441 marypha2lem4 9478 dfoi 9551 r1limg 9811 isf34lem3 10415 compss 10416 fpwwe2lem12 10682 infrenegsup 12251 gsumzf1o 19930 ssidcn 23263 cnco 23274 qtopres 23706 idqtop 23714 qtopcn 23722 mbfid 25670 mbfres 25679 cncombf 25693 dvlog 26693 efopnlem2 26699 seqsval 28294 seqsfn 28315 seqsp1 28317 eucrct2eupth 30264 disjpreima 32597 imadifxp 32614 rinvf1o 32640 suppun2 32693 cyc3genpm 33172 elrgspnsubrunlem2 33252 isconstr 33777 mbfmcst 34261 mbfmco 34266 sitmcl 34353 eulerpartlemt 34373 eulerpartlemmf 34377 eulerpart 34384 0rrv 34453 mclsppslem 35588 bj-iminvid 37196 mptsnun 37340 poimirlem3 37630 ftc1anclem3 37702 areacirclem5 37719 cytpval 43214 arearect 43227 brtrclfv2 43740 0cnf 45892 fourierdlem62 46183 smfco 46817 |
| Copyright terms: Public domain | W3C validator |