Theorem dffn3 6597

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ⊆ wss 3883  ran crn 5581   Fn wfn 6413  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-f 6422

This theorem is referenced by:  ffrn  6598  ffrnb  6599  fsn2  6990  offsplitfpar  7931  fo2ndf  7933  suppcoss  7994  fndmfisuppfi  9070  fndmfifsupp  9071  fin23lem17  10025  fin23lem32  10031  fnct  10224  yoniso  17919  1stckgen  22613  ovolicc2  24591  i1fadd  24764  i1fmul  24765  itg1addlem4  24768  itg1addlem4OLD  24769  i1fmulc  24773  clwlkclwwlklem2  28265  foresf1o  30751  fcoinver  30847  ofpreima2  30905  locfinreflem  31692  pl1cn  31807  fvineqsneu  35509  poimirlem29  35733  poimirlem30  35734  itg2addnclem2  35756  mapdcl  39594  wessf1ornlem  42611  unirnmap  42637  fsneqrn  42640  icccncfext  43318  stoweidlem29  43460  stoweidlem31  43462  stoweidlem59  43490  subsaliuncllem  43786  meadjiunlem  43893  uniimaprimaeqfv  44722  uniimaelsetpreimafv  44736