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

Theorem ima0 5303
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 4970 . 2
2 res0 5232 . . 3
32rneqi 5183 . 2
4 rn0 5208 . 2
51, 3, 43eqtri 2487 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1370   c0 3751  rancrn 4958  |`cres 4959  "cima 4960
This theorem is referenced by:  csbima12  5305  relimasn  5311  elimasni  5315  dffv3  5809  supp0cosupp0  6862  imacosupp  6863  ecexr  7240  domunfican  7719  fodomfi  7725  efgrelexlema  16407  gsumval3OLD  16543  dprdsn  16708  cnindis  19295  cnhaus  19357  cmpfi  19410  xkouni  19571  xkoccn  19591  mbfima  21510  ismbf2d  21519  limcnlp  21753  mdeg0  21941  pserulm  22287  0pth  23938  spthispth  23941  1pthonlem2  23958  eupath2  24070  disjpreima  26396  imadifxp  26407  dstrvprob  27310  opelco3  28045  funpartlem  28429  inisegn0  29856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4530  ax-nul 4538  ax-pr 4648
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rab 2809  df-v 3083  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-br 4410  df-opab 4468  df-xp 4963  df-cnv 4965  df-dm 4967  df-rn 4968  df-res 4969  df-ima 4970
  Copyright terms: Public domain W3C validator