Theorem fnima 6667

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 5676	. 2 ⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴)
2		fnresdm 6656	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
3	2	rneqd 5930	. 2 ⊢ (𝐹 Fn 𝐴 → ran (𝐹 ↾ 𝐴) = ran 𝐹)
4	1, 3	eqtrid 2810	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) = ran 𝐹)

Syntax hints:   → wi 4   = wceq 1570  ran crn 5664   ↾ cres 5665   “ cima 5666   Fn wfn 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-rel 5670  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6540  df-fn 6541

This theorem is referenced by:  infdifsn  9627  cardinfima  10082  alephfp  10093  dprdf1o  20105  dprd2db  20116  rnrhmsubrg  20691  lmhmrnlss  21152  frlmlbs  21928  frlmup3  21931  ellspd  21933  mpfsubrg  22243  pf1subrg  22489  tgrest  23297  uniiccdif  25718  uniioombllem3  25725  dvgt0lem2  26143  f1rnen  32951  cycpmco2rn  33423  r1pquslmic  33878  fedgmul  33999  zarclsint  34240  eulerpartlemn  34749  fineqvinfep  35516  matunitlindflem2  38246  poimirlem15  38264  aks6d1c6lem3  42917  aks6d1c6lem5  42922  aks6d1c7lem1  42925  k0004lem1  44853  3f1oss1  47789  imasetpreimafvbijlemf  48127  fundcmpsurbijinjpreimafv  48133