Theorem fnima 6616

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 5632	. 2 ⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴)
2		fnresdm 6605	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
3	2	rneqd 5882	. 2 ⊢ (𝐹 Fn 𝐴 → ran (𝐹 ↾ 𝐴) = ran 𝐹)
4	1, 3	eqtrid 2780	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) = ran 𝐹)

Syntax hints:   → wi 4   = wceq 1541  ran crn 5620   ↾ cres 5621   “ cima 5622   Fn wfn 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-xp 5625  df-rel 5626  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-fun 6488  df-fn 6489

This theorem is referenced by:  infdifsn  9554  cardinfima  9995  alephfp  10006  dprdf1o  19948  dprd2db  19959  rnrhmsubrg  20522  lmhmrnlss  20986  frlmlbs  21736  frlmup3  21739  ellspd  21741  mpfsubrg  22039  pf1subrg  22264  tgrest  23075  uniiccdif  25507  uniioombllem3  25514  dvgt0lem2  25936  f1rnen  32612  cycpmco2rn  33101  r1pquslmic  33578  fedgmul  33665  zarclsint  33906  eulerpartlemn  34415  matunitlindflem2  37677  poimirlem15  37695  aks6d1c6lem3  42285  aks6d1c6lem5  42290  aks6d1c7lem1  42293  k0004lem1  44264  3f1oss1  47199  imasetpreimafvbijlemf  47525  fundcmpsurbijinjpreimafv  47531