Theorem dffn3 6667

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 3937	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 534	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6489	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 279	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 207   ∧ wa 396   ⊆ wss 3883  ran crn 5619   Fn wfn 6480  ⟶wf 6481

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ss 3900  df-f 6489

This theorem is referenced by:  ffrn  6668  ffrnb  6669  fsn2  7078  coof  7644  offsplitfpar  8058  fo2ndf  8060  suppcoss  8147  fndmfisuppfi  9280  fndmfifsupp  9281  fin23lem17  10251  fin23lem32  10257  fnct  10450  yoniso  18242  psdmplcl  22150  1stckgen  23537  ovolicc2  25507  i1fadd  25680  i1fmul  25681  itg1addlem4  25684  i1fmulc  25688  clwlkclwwlklem2  30088  foresf1o  32592  fcoinver  32693  ofpreima2  32758  fmptunsnop  32792  suppssnn0  32897  locfinreflem  34024  pl1cn  34139  fvineqsneu  37773  poimirlem29  38016  poimirlem30  38017  itg2addnclem2  38039  mapdcl  42145  aks6d1c6isolem2  42660  tfsconcatrev  43793  wessf1ornlem  45632  unirnmap  45653  fsneqrn  45656  icccncfext  46330  stoweidlem29  46472  stoweidlem31  46474  stoweidlem59  46502  subsaliuncllem  46800  meadjiunlem  46908  uniimaprimaeqfv  47857  uniimaelsetpreimafv  47871