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

Theorem ima0 5938
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 5561 . 2 (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2 res0 5850 . . 3 (𝐴 ↾ ∅) = ∅
32rneqi 5800 . 2 ran (𝐴 ↾ ∅) = ran ∅
4 rn0 5789 . 2 ran ∅ = ∅
51, 3, 43eqtri 2846 1 (𝐴 “ ∅) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  c0 4289  ran crn 5549  cres 5550  cima 5551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-opab 5120  df-xp 5554  df-cnv 5556  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561
This theorem is referenced by:  csbima12  5940  relimasn  5945  elimasni  5949  inisegn0  5954  dffv3  6659  suppco  7862  supp0cosupp0  7864  supp0cosupp0OLD  7865  imacosuppOLD  7867  ecexr  8286  domunfican  8783  fodomfi  8789  efgrelexlema  18867  dprdsn  19150  cnindis  21892  cnhaus  21954  cmpfi  22008  xkouni  22199  xkoccn  22219  mbfima  24223  ismbf2d  24233  limcnlp  24468  mdeg0  24656  pserulm  25002  spthispth  27499  pthdlem2  27541  0pth  27896  1pthdlem2  27907  eupth2lemb  28008  disjpreima  30326  imadifxp  30343  swrdrndisj  30624  dstrvprob  31722  opelco3  33011  funpartlem  33396  poimirlem1  34885  poimirlem2  34886  poimirlem3  34887  poimirlem4  34888  poimirlem5  34889  poimirlem6  34890  poimirlem7  34891  poimirlem10  34894  poimirlem11  34895  poimirlem12  34896  poimirlem13  34897  poimirlem16  34900  poimirlem17  34901  poimirlem19  34903  poimirlem20  34904  poimirlem22  34906  poimirlem23  34907  poimirlem24  34908  poimirlem25  34909  poimirlem28  34912  poimirlem29  34913  poimirlem31  34915  he0  40120  smfresal  43053
  Copyright terms: Public domain W3C validator