![]() |
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 6074 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1536 “ cima 5691 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5148 df-opab 5210 df-cnv 5696 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 |
This theorem is referenced by: mptpreima 6259 csbpredg 6328 isarep2 6658 suppun 8207 suppco 8229 fsuppun 9424 fsuppcolem 9438 marypha2lem4 9475 dfoi 9548 r1limg 9808 isf34lem3 10412 compss 10413 fpwwe2lem12 10679 infrenegsup 12248 gsumzf1o 19944 ssidcn 23278 cnco 23289 qtopres 23721 idqtop 23729 qtopcn 23737 mbfid 25683 mbfres 25692 cncombf 25706 dvlog 26707 efopnlem2 26713 seqsval 28308 seqsfn 28329 seqsp1 28331 eucrct2eupth 30273 disjpreima 32603 imadifxp 32620 rinvf1o 32646 suppun2 32698 cyc3genpm 33154 mbfmcst 34240 mbfmco 34245 sitmcl 34332 eulerpartlemt 34352 eulerpartlemmf 34356 eulerpart 34363 0rrv 34432 mclsppslem 35567 bj-iminvid 37177 mptsnun 37321 poimirlem3 37609 ftc1anclem3 37681 areacirclem5 37698 cytpval 43190 arearect 43203 brtrclfv2 43716 0cnf 45832 fourierdlem62 46123 smfco 46757 |
Copyright terms: Public domain | W3C validator |