![]() |
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 6054 | . 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-cnv 5684 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 |
This theorem is referenced by: mptpreima 6237 csbpredg 6306 isarep2 6639 suppun 8174 suppco 8197 fsuppun 9388 fsuppcolem 9402 marypha2lem4 9439 dfoi 9512 r1limg 9772 isf34lem3 10376 compss 10377 fpwwe2lem12 10643 infrenegsup 12204 gsumzf1o 19828 ssidcn 23079 cnco 23090 qtopres 23522 idqtop 23530 qtopcn 23538 mbfid 25484 mbfres 25493 cncombf 25507 dvlog 26499 efopnlem2 26505 eucrct2eupth 29932 disjpreima 32249 imadifxp 32266 rinvf1o 32288 cyc3genpm 32748 mbfmcst 33723 mbfmco 33728 sitmcl 33815 eulerpartlemt 33835 eulerpartlemmf 33839 eulerpart 33846 0rrv 33915 mclsppslem 35039 bj-iminvid 36542 mptsnun 36686 poimirlem3 36957 ftc1anclem3 37029 areacirclem5 37046 cytpval 42416 arearect 42429 brtrclfv2 42943 0cnf 45054 fourierdlem62 45345 smfco 45979 |
Copyright terms: Public domain | W3C validator |