Theorem fnima 6661

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 5664	. 2 ⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴)
2		fnresdm 6650	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
3	2	rneqd 5920	. 2 ⊢ (𝐹 Fn 𝐴 → ran (𝐹 ↾ 𝐴) = ran 𝐹)
4	1, 3	eqtrid 2808	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) = ran 𝐹)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5652   ↾ cres 5653   “ cima 5654   Fn wfn 6526

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6533  df-fn 6534

This theorem is used by:  infdifsn  9642  cardinfima  10157  alephfp  10168  dprdf1o  20228  dprd2db  20239  rnrhmsubrg  20837  lmhmrnlss  21305  frlmlbs  22083  frlmup3  22086  ellspd  22088  mpfsubrg  22400  pf1subrg  22646  matunitlindflem2  22975  tgrest  23457  uniiccdif  25879  uniioombllem3  25886  dvgt0lem2  26303  f1rnen  33204  cycpmco2rn  33668  r1pquslmic  34124  fedgmul  34245  zarclsint  34486  eulerpartlemn  34996  fineqvinfep  35766  poimirlem15  38521  aks6d1c6lem3  43190  aks6d1c6lem5  43195  aks6d1c7lem1  43198  k0004lem1  45106  tmachlem-franscan  47903  3f1oss1  48089  imasetpreimafvbijlemf  48427  fundcmpsurbijinjpreimafv  48433