Theorem dffn3 6680

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3889  ran crn 5632   Fn wfn 6493  ⟶wf 6494

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3906  df-f 6502

This theorem is referenced by:  ffrn  6681  ffrnb  6682  fsn2  7089  coof  7655  offsplitfpar  8069  fo2ndf  8071  suppcoss  8157  fndmfisuppfi  9290  fndmfifsupp  9291  fin23lem17  10260  fin23lem32  10266  fnct  10459  yoniso  18251  psdmplcl  22128  1stckgen  23519  ovolicc2  25489  i1fadd  25662  i1fmul  25663  itg1addlem4  25666  i1fmulc  25670  clwlkclwwlklem2  30070  foresf1o  32574  fcoinver  32674  ofpreima2  32739  fmptunsnop  32773  suppssnn0  32878  locfinreflem  33984  pl1cn  34099  fvineqsneu  37727  poimirlem29  37970  poimirlem30  37971  itg2addnclem2  37993  mapdcl  42099  aks6d1c6isolem2  42614  tfsconcatrev  43776  wessf1ornlem  45615  unirnmap  45637  fsneqrn  45640  icccncfext  46315  stoweidlem29  46457  stoweidlem31  46459  stoweidlem59  46487  subsaliuncllem  46785  meadjiunlem  46893  uniimaprimaeqfv  47842  uniimaelsetpreimafv  47856