![]() |
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 5156 | . 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅) | |
2 | res0 5432 | . . 3 ⊢ (𝐴 ↾ ∅) = ∅ | |
3 | 2 | rneqi 5384 | . 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅ |
4 | rn0 5409 | . 2 ⊢ ran ∅ = ∅ | |
5 | 1, 3, 4 | 3eqtri 2677 | 1 ⊢ (𝐴 “ ∅) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ∅c0 3948 ran crn 5144 ↾ cres 5145 “ cima 5146 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-opab 4746 df-xp 5149 df-cnv 5151 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 |
This theorem is referenced by: csbima12 5518 relimasn 5523 elimasni 5527 inisegn0 5532 dffv3 6225 supp0cosupp0 7379 imacosupp 7380 ecexr 7792 domunfican 8274 fodomfi 8280 efgrelexlema 18208 dprdsn 18481 cnindis 21144 cnhaus 21206 cmpfi 21259 xkouni 21450 xkoccn 21470 mbfima 23444 ismbf2d 23453 limcnlp 23687 mdeg0 23875 pserulm 24221 spthispth 26678 pthdlem2 26720 0pth 27103 1pthdlem2 27114 eupth2lemb 27215 disjpreima 29523 imadifxp 29540 dstrvprob 30661 opelco3 31802 funpartlem 32174 poimirlem1 33540 poimirlem2 33541 poimirlem3 33542 poimirlem4 33543 poimirlem5 33544 poimirlem6 33545 poimirlem7 33546 poimirlem10 33549 poimirlem11 33550 poimirlem12 33551 poimirlem13 33552 poimirlem16 33555 poimirlem17 33556 poimirlem19 33558 poimirlem20 33559 poimirlem22 33561 poimirlem23 33562 poimirlem24 33563 poimirlem25 33564 poimirlem28 33567 poimirlem29 33568 poimirlem31 33570 he0 38395 smfresal 41316 |
Copyright terms: Public domain | W3C validator |