Theorem fnima 6666

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	⊢ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) = ran 𝐹)

Proof of Theorem fnima

Step	Hyp	Ref	Expression
1		df-ima 5672	. 2 ⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴)
2		fnresdm 6655	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
3	2	rneqd 5926	. 2 ⊢ (𝐹 Fn 𝐴 → ran (𝐹 ↾ 𝐴) = ran 𝐹)
4	1, 3	eqtrid 2809	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) = ran 𝐹)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5660   ↾ cres 5661   “ cima 5662   Fn wfn 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-rel 5666  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6539  df-fn 6540

This theorem is used by:  infdifsn  9640  cardinfima  10104  alephfp  10115  dprdf1o  20167  dprd2db  20178  rnrhmsubrg  20773  lmhmrnlss  21240  frlmlbs  22016  frlmup3  22019  ellspd  22021  mpfsubrg  22333  pf1subrg  22579  matunitlindflem2  22908  tgrest  23390  uniiccdif  25812  uniioombllem3  25819  dvgt0lem2  26237  f1rnen  33109  cycpmco2rn  33573  r1pquslmic  34028  fedgmul  34149  zarclsint  34390  eulerpartlemn  34900  fineqvinfep  35659  poimirlem15  38392  aks6d1c6lem3  43046  aks6d1c6lem5  43051  aks6d1c7lem1  43054  k0004lem1  44995  tmachlem-franscan  47785  3f1oss1  47971  imasetpreimafvbijlemf  48309  fundcmpsurbijinjpreimafv  48315