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 5602 | . 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅) | |
2 | res0 5895 | . . 3 ⊢ (𝐴 ↾ ∅) = ∅ | |
3 | 2 | rneqi 5846 | . 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅ |
4 | rn0 5835 | . 2 ⊢ ran ∅ = ∅ | |
5 | 1, 3, 4 | 3eqtri 2770 | 1 ⊢ (𝐴 “ ∅) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∅c0 4256 ran crn 5590 ↾ cres 5591 “ cima 5592 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-br 5075 df-opab 5137 df-xp 5595 df-cnv 5597 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 |
This theorem is referenced by: csbima12 5987 relimasn 5992 elimasni 5999 inisegn0 6006 predprc 6241 dffv3 6770 suppco 8022 supp0cosupp0 8024 ecexr 8503 imafi 8958 domunfican 9087 fodomfi 9092 efgrelexlema 19355 dprdsn 19639 cnindis 22443 cnhaus 22505 cmpfi 22559 xkouni 22750 xkoccn 22770 mbfima 24794 ismbf2d 24804 limcnlp 25042 mdeg0 25235 pserulm 25581 spthispth 28094 pthdlem2 28136 0pth 28489 1pthdlem2 28500 eupth2lemb 28601 disjpreima 30923 imadifxp 30940 2ndimaxp 30984 swrdrndisj 31229 gsumpart 31315 zarclsint 31822 dstrvprob 32438 opelco3 33749 old0 34043 made0 34057 negs0s 34124 funpartlem 34244 poimirlem1 35778 poimirlem2 35779 poimirlem3 35780 poimirlem4 35781 poimirlem5 35782 poimirlem6 35783 poimirlem7 35784 poimirlem10 35787 poimirlem11 35788 poimirlem12 35789 poimirlem13 35790 poimirlem16 35793 poimirlem17 35794 poimirlem19 35796 poimirlem20 35797 poimirlem22 35799 poimirlem23 35800 poimirlem24 35801 poimirlem25 35802 poimirlem28 35805 poimirlem29 35806 poimirlem31 35808 he0 41392 smfresal 44322 predisj 46156 |
Copyright terms: Public domain | W3C validator |