Theorem fnima 6710

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 5713	. 2 ⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴)
2		fnresdm 6699	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
3	2	rneqd 5963	. 2 ⊢ (𝐹 Fn 𝐴 → ran (𝐹 ↾ 𝐴) = ran 𝐹)
4	1, 3	eqtrid 2792	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) = ran 𝐹)

Syntax hints:   → wi 4   = wceq 1537  ran crn 5701   ↾ cres 5702   “ cima 5703   Fn wfn 6568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707  df-cnv 5708  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-fun 6575  df-fn 6576

This theorem is referenced by:  infdifsn  9726  cardinfima  10166  alephfp  10177  dprdf1o  20076  dprd2db  20087  rnrhmsubrg  20633  lmhmrnlss  21072  frlmlbs  21840  frlmup3  21843  ellspd  21845  mpfsubrg  22150  pf1subrg  22373  tgrest  23188  uniiccdif  25632  uniioombllem3  25639  dvgt0lem2  26062  f1rnen  32648  cycpmco2rn  33118  r1pquslmic  33596  fedgmul  33644  zarclsint  33818  eulerpartlemn  34346  matunitlindflem2  37577  poimirlem15  37595  aks6d1c6lem3  42129  aks6d1c6lem5  42134  aks6d1c7lem1  42137  k0004lem1  44109  3f1oss1  46990  imasetpreimafvbijlemf  47275  fundcmpsurbijinjpreimafv  47281