Theorem dffn3 6664

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 3958	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 529	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6486	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 278	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3903  ran crn 5620   Fn wfn 6477  ⟶wf 6478

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3920  df-f 6486

This theorem is referenced by:  ffrn  6665  ffrnb  6666  fsn2  7070  coof  7637  offsplitfpar  8052  fo2ndf  8054  suppcoss  8140  fndmfisuppfi  9267  fndmfifsupp  9268  fin23lem17  10232  fin23lem32  10238  fnct  10431  yoniso  18191  psdmplcl  22047  1stckgen  23439  ovolicc2  25421  i1fadd  25594  i1fmul  25595  itg1addlem4  25598  i1fmulc  25602  clwlkclwwlklem2  29944  foresf1o  32448  fcoinver  32548  ofpreima2  32609  fmptunsnop  32642  suppssnn0  32750  locfinreflem  33807  pl1cn  33922  fvineqsneu  37385  poimirlem29  37629  poimirlem30  37630  itg2addnclem2  37652  mapdcl  41632  aks6d1c6isolem2  42148  tfsconcatrev  43321  wessf1ornlem  45163  unirnmap  45186  fsneqrn  45189  icccncfext  45868  stoweidlem29  46010  stoweidlem31  46012  stoweidlem59  46040  subsaliuncllem  46338  meadjiunlem  46446  uniimaprimaeqfv  47366  uniimaelsetpreimafv  47380