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 5917 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 “ cima 5551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-opab 5120 df-cnv 5556 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 |
This theorem is referenced by: mptpreima 6085 isarep2 6436 suppun 7839 suppco 7859 supp0cosupp0OLD 7862 imacosuppOLD 7864 fsuppun 8840 fsuppcolem 8852 marypha2lem4 8890 dfoi 8963 r1limg 9188 isf34lem3 9785 compss 9786 fpwwe2lem13 10052 infrenegsup 11612 gsumzf1o 18961 ssidcn 21791 cnco 21802 qtopres 22234 idqtop 22242 qtopcn 22250 mbfid 24163 mbfres 24172 cncombf 24186 dvlog 25161 efopnlem2 25167 eucrct2eupth 27951 disjpreima 30262 imadifxp 30279 rinvf1o 30303 cyc3genpm 30721 mbfmcst 31416 mbfmco 31421 sitmcl 31508 eulerpartlemt 31528 eulerpartlemmf 31532 eulerpart 31539 0rrv 31608 mclsppslem 32727 csbpredg 34489 mptsnun 34502 poimirlem3 34776 ftc1anclem3 34850 areacirclem5 34867 cytpval 39687 arearect 39700 brtrclfv2 39950 0cnf 42036 fourierdlem62 42330 smfco 42954 |
Copyright terms: Public domain | W3C validator |