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

Theorem fnima 5399
Description: The image of a function's domain is its range. (Contributed by NM, 4-Nov-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Assertion
Ref Expression
fnima  |-  ( F  Fn  A  ->  ( F " A )  =  ran  F )

Proof of Theorem fnima
StepHypRef Expression
1 df-ima 4739 . 2  |-  ( F
" A )  =  ran  ( F  |`  A )
2 fnresdm 5390 . . 3  |-  ( F  Fn  A  ->  ( F  |`  A )  =  F )
32rneqd 4943 . 2  |-  ( F  Fn  A  ->  ran  ( F  |`  A )  =  ran  F )
41, 3syl5eq 2360 1  |-  ( F  Fn  A  ->  ( F " A )  =  ran  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1633   ran crn 4727    |` cres 4728   "cima 4729    Fn wfn 5287
This theorem is referenced by:  infdifsn  7402  carduniima  7768  cardinfima  7769  alephfp  7780  dprdf1o  15316  dprd2db  15327  lmhmrnlss  15856  tgrest  16946  uniiccdif  18986  uniioombllem3  18993  dvgt0lem2  19403  mpfsubrg  19477  pf1subrg  19484  frlmlbs  26397  frlmup3  26400  ellspd  26402
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-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  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-rel 4733  df-cnv 4734  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-fun 5294  df-fn 5295
  Copyright terms: Public domain W3C validator