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

Theorem ima0 5067
Description: Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.)
Assertion
Ref Expression
ima0  |-  ( A
" (/) )  =  (/)

Proof of Theorem ima0
StepHypRef Expression
1 df-ima 4739 . 2  |-  ( A
" (/) )  =  ran  ( A  |`  (/) )
2 res0 4996 . . 3  |-  ( A  |`  (/) )  =  (/)
32rneqi 4942 . 2  |-  ran  ( A  |`  (/) )  =  ran  (/)
4 rn0 4973 . 2  |-  ran  (/)  =  (/)
51, 3, 43eqtri 2340 1  |-  ( A
" (/) )  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1633   (/)c0 3489   ran crn 4727    |` cres 4728   "cima 4729
This theorem is referenced by:  relimasn  5073  elimasni  5077  dffv3  5559  ecexr  6707  domunfican  7174  fodomfi  7180  efgrelexlema  15107  gsumval3  15240  dprdsn  15320  cnindis  17076  cnhaus  17138  cmpfi  17191  xkouni  17350  xkoccn  17369  mbfima  19040  ismbf2d  19049  limcnlp  19281  mdeg0  19509  pserulm  19851  disjpreima  23169  imadifxp  23187  dstrvprob  23903  eupath2  24188  funpartlem  24866  inisegn0  26288  0pth  27472  spthispth  27475  1pthonlem2  27486
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-br 4061  df-opab 4115  df-xp 4732  df-cnv 4734  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739
  Copyright terms: Public domain W3C validator