Theorem dffn3 6675

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3890  ran crn 5626   Fn wfn 6488  ⟶wf 6489

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 3907  df-f 6497

This theorem is referenced by:  ffrn  6676  ffrnb  6677  fsn2  7084  coof  7649  offsplitfpar  8063  fo2ndf  8065  suppcoss  8151  fndmfisuppfi  9284  fndmfifsupp  9285  fin23lem17  10254  fin23lem32  10260  fnct  10453  yoniso  18245  psdmplcl  22141  1stckgen  23532  ovolicc2  25502  i1fadd  25675  i1fmul  25676  itg1addlem4  25679  i1fmulc  25683  clwlkclwwlklem2  30088  foresf1o  32592  fcoinver  32692  ofpreima2  32757  fmptunsnop  32791  suppssnn0  32896  locfinreflem  34003  pl1cn  34118  fvineqsneu  37744  poimirlem29  37987  poimirlem30  37988  itg2addnclem2  38010  mapdcl  42116  aks6d1c6isolem2  42631  tfsconcatrev  43797  wessf1ornlem  45636  unirnmap  45658  fsneqrn  45661  icccncfext  46336  stoweidlem29  46478  stoweidlem31  46480  stoweidlem59  46508  subsaliuncllem  46806  meadjiunlem  46914  uniimaprimaeqfv  47857  uniimaelsetpreimafv  47871