Theorem dffn3 6682

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

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

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 3928  df-f 6503

This theorem is referenced by:  ffrn  6683  ffrnb  6684  fsn2  7090  coof  7657  offsplitfpar  8075  fo2ndf  8077  suppcoss  8163  fndmfisuppfi  9304  fndmfifsupp  9305  fin23lem17  10267  fin23lem32  10273  fnct  10466  yoniso  18222  psdmplcl  22025  1stckgen  23417  ovolicc2  25399  i1fadd  25572  i1fmul  25573  itg1addlem4  25576  i1fmulc  25580  clwlkclwwlklem2  29902  foresf1o  32406  fcoinver  32506  ofpreima2  32563  fmptunsnop  32596  suppssnn0  32703  locfinreflem  33803  pl1cn  33918  fvineqsneu  37372  poimirlem29  37616  poimirlem30  37617  itg2addnclem2  37639  mapdcl  41620  aks6d1c6isolem2  42136  tfsconcatrev  43310  wessf1ornlem  45152  unirnmap  45175  fsneqrn  45178  icccncfext  45858  stoweidlem29  46000  stoweidlem31  46002  stoweidlem59  46030  subsaliuncllem  46328  meadjiunlem  46436  uniimaprimaeqfv  47356  uniimaelsetpreimafv  47370