Theorem dffn3 6671

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3898  ran crn 5622   Fn wfn 6484  ⟶wf 6485

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3915  df-f 6493

This theorem is referenced by:  ffrn  6672  ffrnb  6673  fsn2  7078  coof  7643  offsplitfpar  8058  fo2ndf  8060  suppcoss  8146  fndmfisuppfi  9272  fndmfifsupp  9273  fin23lem17  10240  fin23lem32  10246  fnct  10439  yoniso  18199  psdmplcl  22096  1stckgen  23489  ovolicc2  25470  i1fadd  25643  i1fmul  25644  itg1addlem4  25647  i1fmulc  25651  clwlkclwwlklem2  30001  foresf1o  32505  fcoinver  32605  ofpreima2  32670  fmptunsnop  32705  suppssnn0  32813  locfinreflem  33925  pl1cn  34040  fvineqsneu  37528  poimirlem29  37762  poimirlem30  37763  itg2addnclem2  37785  mapdcl  41825  aks6d1c6isolem2  42341  tfsconcatrev  43505  wessf1ornlem  45345  unirnmap  45368  fsneqrn  45371  icccncfext  46047  stoweidlem29  46189  stoweidlem31  46191  stoweidlem59  46219  subsaliuncllem  46517  meadjiunlem  46625  uniimaprimaeqfv  47544  uniimaelsetpreimafv  47558