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  8113  fo2ndf  8115  suppcoss  8202  fndmfisuppfi  9336  fndmfifsupp  9337  fin23lem17  10321  fin23lem32  10327  fnct  10520  yoniso  18340  psdmplcl  22293  1stckgen  23679  ovolicc2  25649  i1fadd  25822  i1fmul  25823  itg1addlem4  25826  i1fmulc  25830  clwlkclwwlklem2  30291  foresf1o  32790  fcoinver  32889  ofpreima2  32951  fmptunsnop  32985  suppssnn0  33090  locfinreflem  34174  pl1cn  34289  fvineqsneu  37944  poimirlem29  38187  poimirlem30  38188  itg2addnclem2  38210  mapdcl  42316  aks6d1c6isolem2  42831  tfsconcatrev  43966  wessf1ornlem  45794  unirnmap  45815  fsneqrn  45818  icccncfext  46492  stoweidlem29  46634  stoweidlem31  46636  stoweidlem59  46664  subsaliuncllem  46962  meadjiunlem  47070  uniimaprimaeqfv  48019  uniimaelsetpreimafv  48033