Theorem dffn3 6759

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3976  ran crn 5701   Fn wfn 6568  ⟶wf 6569

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3993  df-f 6577

This theorem is referenced by:  ffrn  6760  ffrnb  6761  fsn2  7170  coof  7737  offsplitfpar  8160  fo2ndf  8162  suppcoss  8248  fndmfisuppfi  9446  fndmfifsupp  9447  fin23lem17  10407  fin23lem32  10413  fnct  10606  yoniso  18355  psdmplcl  22189  1stckgen  23583  ovolicc2  25576  i1fadd  25749  i1fmul  25750  itg1addlem4  25753  itg1addlem4OLD  25754  i1fmulc  25758  clwlkclwwlklem2  30032  foresf1o  32532  fcoinver  32626  ofpreima2  32684  suppssnn0  32812  locfinreflem  33786  pl1cn  33901  fvineqsneu  37377  poimirlem29  37609  poimirlem30  37610  itg2addnclem2  37632  mapdcl  41610  aks6d1c6isolem2  42132  tfsconcatrev  43310  wessf1ornlem  45092  unirnmap  45115  fsneqrn  45118  icccncfext  45808  stoweidlem29  45950  stoweidlem31  45952  stoweidlem59  45980  subsaliuncllem  46278  meadjiunlem  46386  uniimaprimaeqfv  47256  uniimaelsetpreimafv  47270