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

Theorem ima0 5156
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 4824 . 2
2 res0 5086 . . 3
32rneqi 5037 . 2
4 rn0 5062 . 2
51, 3, 43eqtri 2446 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1687   c0 3614  rancrn 4812  |`cres 4813  "cima 4814
This theorem is referenced by:  csbima12  5158  relimasn  5164  elimasni  5168  dffv3  5657  ecexr  7067  domunfican  7543  fodomfi  7549  efgrelexlema  16183  gsumval3  16317  dprdsn  16403  cnindis  18600  cnhaus  18662  cmpfi  18715  xkouni  18876  xkoccn  18896  mbfima  20810  ismbf2d  20819  limcnlp  21053  mdeg0  21283  pserulm  21628  0pth  23148  spthispth  23151  1pthonlem2  23168  eupath2  23280  disjpreima  25608  imadifxp  25619  dstrvprob  26557  opelco3  27291  funpartlem  27675  inisegn0  29069  supp0cosupp0  30441  imacosupp  30442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pr 4503
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-br 4268  df-opab 4326  df-xp 4817  df-cnv 4819  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824
  Copyright terms: Public domain W3C validator