| 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 5633 | . 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅) | |
| 2 | res0 5937 | . . 3 ⊢ (𝐴 ↾ ∅) = ∅ | |
| 3 | 2 | rneqi 5881 | . 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅ |
| 4 | rn0 5870 | . 2 ⊢ ran ∅ = ∅ | |
| 5 | 1, 3, 4 | 3eqtri 2762 | 1 ⊢ (𝐴 “ ∅) = ∅ |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1542 ∅c0 4263 ran crn 5621 ↾ cres 5622 “ cima 5623 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2707 ax-sep 5220 ax-pr 5364 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2714 df-cleq 2727 df-clel 2810 df-rab 3388 df-v 3429 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-nul 4264 df-if 4457 df-sn 4558 df-pr 4560 df-op 4564 df-br 5075 df-opab 5137 df-xp 5626 df-cnv 5628 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 |
| This theorem is referenced by: csbima12 6033 relimasn 6039 elimasni 6045 inisegn0 6052 predprc 6291 dffv3 6825 suppco 8145 supp0cosupp0 8147 ecexr 8637 fodomfi 9211 imafiOLD 9215 domunfican 9221 fodomfiOLD 9229 efgrelexlema 19713 dprdsn 20002 cnindis 23245 cnhaus 23307 cmpfi 23361 xkouni 23552 xkoccn 23572 mbfima 25585 ismbf2d 25595 limcnlp 25833 mdeg0 26023 pserulm 26375 old0 27819 made0 27843 neg0s 28006 neg1s 28007 zcuts0 28388 spthispth 29780 dfpth2 29785 pthdlem2 29824 0pth 30183 1pthdlem2 30194 eupth2lemb 30295 disjpreima 32642 imadifxp 32659 2ndimaxp 32707 mptiffisupp 32754 swrdrndisj 33005 gsumpart 33112 esplyfval2 33697 zarclsint 34004 dstrvprob 34604 opelco3 35945 funpartlem 36112 poimirlem1 37930 poimirlem2 37931 poimirlem3 37932 poimirlem4 37933 poimirlem5 37934 poimirlem6 37935 poimirlem7 37936 poimirlem10 37939 poimirlem11 37940 poimirlem12 37941 poimirlem13 37942 poimirlem16 37945 poimirlem17 37946 poimirlem19 37948 poimirlem20 37949 poimirlem22 37951 poimirlem23 37952 poimirlem24 37953 poimirlem25 37954 poimirlem28 37957 poimirlem29 37958 poimirlem31 37960 he0 44199 smfresal 47204 predisj 49274 |
| Copyright terms: Public domain | W3C validator |