![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ima0 | Structured version Visualization version GIF version |
Description: Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.) |
Ref | Expression |
---|---|
ima0 | ⊢ (𝐴 “ ∅) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ima 5323 | . 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅) | |
2 | res0 5602 | . . 3 ⊢ (𝐴 ↾ ∅) = ∅ | |
3 | 2 | rneqi 5553 | . 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅ |
4 | rn0 5579 | . 2 ⊢ ran ∅ = ∅ | |
5 | 1, 3, 4 | 3eqtri 2823 | 1 ⊢ (𝐴 “ ∅) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1653 ∅c0 4113 ran crn 5311 ↾ cres 5312 “ cima 5313 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-sep 4973 ax-nul 4981 ax-pr 5095 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-rab 3096 df-v 3385 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-sn 4367 df-pr 4369 df-op 4373 df-br 4842 df-opab 4904 df-xp 5316 df-cnv 5318 df-dm 5320 df-rn 5321 df-res 5322 df-ima 5323 |
This theorem is referenced by: csbima12 5698 relimasn 5703 elimasni 5707 inisegn0 5712 dffv3 6405 supp0cosupp0 7570 imacosupp 7571 ecexr 7985 domunfican 8473 fodomfi 8479 efgrelexlema 18474 dprdsn 18748 cnindis 21422 cnhaus 21484 cmpfi 21537 xkouni 21728 xkoccn 21748 mbfima 23735 ismbf2d 23745 limcnlp 23980 mdeg0 24168 pserulm 24514 spthispth 26972 pthdlem2 27014 0pth 27461 1pthdlem2 27472 eupth2lemb 27574 disjpreima 29906 imadifxp 29923 dstrvprob 31042 opelco3 32182 funpartlem 32554 poimirlem1 33891 poimirlem2 33892 poimirlem3 33893 poimirlem4 33894 poimirlem5 33895 poimirlem6 33896 poimirlem7 33897 poimirlem10 33900 poimirlem11 33901 poimirlem12 33902 poimirlem13 33903 poimirlem16 33906 poimirlem17 33907 poimirlem19 33909 poimirlem20 33910 poimirlem22 33912 poimirlem23 33913 poimirlem24 33914 poimirlem25 33915 poimirlem28 33918 poimirlem29 33919 poimirlem31 33921 he0 38848 smfresal 41729 |
Copyright terms: Public domain | W3C validator |