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

Theorem ima0 5145
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 4809 . 2  |-  ( A
" (/) )  =  ran  ( A  |`  (/) )
2 res0 5071 . . 3  |-  ( A  |`  (/) )  =  (/)
32rneqi 5023 . 2  |-  ran  ( A  |`  (/) )  =  ran  (/)
4 rn0 5048 . 2  |-  ran  (/)  =  (/)
51, 3, 43eqtri 2454 1  |-  ( A
" (/) )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   (/)c0 3704   ran crn 4797    |` cres 4798   "cima 4799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-br 4367  df-opab 4426  df-xp 4802  df-cnv 4804  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809
This theorem is referenced by:  csbima12  5147  relimasn  5153  elimasni  5157  inisegn0  5162  dffv3  5821  supp0cosupp0  6909  imacosupp  6910  ecexr  7323  domunfican  7797  fodomfi  7803  efgrelexlema  17342  dprdsn  17612  cnindis  20250  cnhaus  20312  cmpfi  20365  xkouni  20556  xkoccn  20576  mbfima  22530  ismbf2d  22539  limcnlp  22775  mdeg0  22961  pserulm  23319  0pth  25242  spthispth  25245  1pthonlem2  25262  eupath2  25650  disjpreima  28140  imadifxp  28158  dstrvprob  29256  opelco3  30371  funpartlem  30658  poimirlem1  31848  poimirlem2  31849  poimirlem3  31850  poimirlem4  31851  poimirlem5  31852  poimirlem6  31853  poimirlem7  31854  poimirlem10  31857  poimirlem11  31858  poimirlem12  31859  poimirlem13  31860  poimirlem16  31863  poimirlem17  31864  poimirlem19  31866  poimirlem20  31867  poimirlem22  31869  poimirlem23  31870  poimirlem24  31871  poimirlem25  31872  poimirlem28  31875  poimirlem29  31876  poimirlem31  31878  he0  36293
  Copyright terms: Public domain W3C validator