Theorem dffn3 6731

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ⊆ wss 3949  ran crn 5678   Fn wfn 6539  ⟶wf 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-f 6548

This theorem is referenced by:  ffrn  6732  ffrnb  6733  fsn2  7134  offsplitfpar  8105  fo2ndf  8107  suppcoss  8192  fndmfisuppfi  9375  fndmfifsupp  9376  fin23lem17  10333  fin23lem32  10339  fnct  10532  yoniso  18238  1stckgen  23058  ovolicc2  25039  i1fadd  25212  i1fmul  25213  itg1addlem4  25216  itg1addlem4OLD  25217  i1fmulc  25221  clwlkclwwlklem2  29253  foresf1o  31742  fcoinver  31835  ofpreima2  31891  suppssnn0  32017  locfinreflem  32820  pl1cn  32935  fvineqsneu  36292  poimirlem29  36517  poimirlem30  36518  itg2addnclem2  36540  mapdcl  40524  tfsconcatrev  42098  wessf1ornlem  43882  unirnmap  43907  fsneqrn  43910  icccncfext  44603  stoweidlem29  44745  stoweidlem31  44747  stoweidlem59  44775  subsaliuncllem  45073  meadjiunlem  45181  uniimaprimaeqfv  46050  uniimaelsetpreimafv  46064