MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ima0 Structured version   Visualization version   GIF version

Theorem ima0 6033
Description: Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.)
Assertion
Ref Expression
ima0 (𝐴 “ ∅) = ∅

Proof of Theorem ima0
StepHypRef Expression
1 df-ima 5650 . 2 (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2 res0 5945 . . 3 (𝐴 ↾ ∅) = ∅
32rneqi 5896 . 2 ran (𝐴 ↾ ∅) = ran ∅
4 rn0 5885 . 2 ran ∅ = ∅
51, 3, 43eqtri 2765 1 (𝐴 “ ∅) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  c0 4286  ran crn 5638  cres 5639  cima 5640
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pr 5388
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-br 5110  df-opab 5172  df-xp 5643  df-cnv 5645  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650
This theorem is referenced by:  csbima12  6035  relimasn  6040  elimasni  6047  inisegn0  6054  predprc  6296  dffv3  6842  suppco  8141  supp0cosupp0  8143  ecexr  8659  imafi  9125  domunfican  9270  fodomfi  9275  efgrelexlema  19539  dprdsn  19823  cnindis  22666  cnhaus  22728  cmpfi  22782  xkouni  22973  xkoccn  22993  mbfima  25017  ismbf2d  25027  limcnlp  25265  mdeg0  25458  pserulm  25804  old0  27218  made0  27232  negs0s  27354  spthispth  28723  pthdlem2  28765  0pth  29118  1pthdlem2  29129  eupth2lemb  29230  disjpreima  31555  imadifxp  31572  2ndimaxp  31616  mptiffisupp  31661  swrdrndisj  31867  gsumpart  31953  zarclsint  32517  dstrvprob  33135  opelco3  34412  funpartlem  34580  poimirlem1  36129  poimirlem2  36130  poimirlem3  36131  poimirlem4  36132  poimirlem5  36133  poimirlem6  36134  poimirlem7  36135  poimirlem10  36138  poimirlem11  36139  poimirlem12  36140  poimirlem13  36141  poimirlem16  36144  poimirlem17  36145  poimirlem19  36147  poimirlem20  36148  poimirlem22  36150  poimirlem23  36151  poimirlem24  36152  poimirlem25  36153  poimirlem28  36156  poimirlem29  36157  poimirlem31  36159  he0  42148  smfresal  45119  predisj  46985
  Copyright terms: Public domain W3C validator