Theorem dffn3 6719

Description: A function maps to its range. (Contributed by NM, 1-Sep-1999.)

Assertion

Ref	Expression
dffn3	⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Proof of Theorem dffn3

Step	Hyp	Ref	Expression
1		ssid 3967	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 538	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6541	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 281	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 209   ∧ wa 400   ⊆ wss 3913  ran crn 5663   Fn wfn 6532  ⟶wf 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3930  df-f 6541

This theorem is referenced by:  ffrn  6720  ffrnb  6721  fsn2  7133  coof  7699  offsplitfpar  8114  fo2ndf  8116  suppcoss  8203  fndmfisuppfi  9337  fndmfifsupp  9338  fin23lem17  10322  fin23lem32  10328  fnct  10521  yoniso  18341  psdmplcl  22294  1stckgen  23680  ovolicc2  25650  i1fadd  25823  i1fmul  25824  itg1addlem4  25827  i1fmulc  25831  clwlkclwwlklem2  30292  foresf1o  32791  fcoinver  32890  ofpreima2  32952  fmptunsnop  32986  suppssnn0  33091  locfinreflem  34175  pl1cn  34290  fvineqsneu  37945  poimirlem29  38188  poimirlem30  38189  itg2addnclem2  38211  mapdcl  42317  aks6d1c6isolem2  42832  tfsconcatrev  43967  wessf1ornlem  45795  unirnmap  45816  fsneqrn  45819  icccncfext  46493  stoweidlem29  46635  stoweidlem31  46637  stoweidlem59  46665  subsaliuncllem  46963  meadjiunlem  47071  uniimaprimaeqfv  48020  uniimaelsetpreimafv  48034