Theorem dffn3 6718

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 3959	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 538	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6540	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 281	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 209   ∧ wa 400   ⊆ wss 3905  ran crn 5662   Fn wfn 6531  ⟶wf 6532

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3922  df-f 6540

This theorem is referenced by:  ffrn  6719  ffrnb  6720  fsn2  7132  coof  7698  offsplitfpar  8110  fo2ndf  8112  suppcoss  8199  fndmfisuppfi  9333  fndmfifsupp  9334  fin23lem17  10317  fin23lem32  10323  fnct  10516  yoniso  18336  psdmplcl  22325  1stckgen  23711  ovolicc2  25681  i1fadd  25854  i1fmul  25855  itg1addlem4  25858  i1fmulc  25862  clwlkclwwlklem2  30351  foresf1o  32850  fcoinver  32949  ofpreima2  33011  fmptunsnop  33045  suppssnn0  33150  locfinreflem  34230  pl1cn  34345  fvineqsneu  38077  poimirlem29  38320  poimirlem30  38321  itg2addnclem2  38343  mapdcl  42447  aks6d1c6isolem2  42962  tfsconcatrev  44095  wessf1ornlem  45923  unirnmap  45944  fsneqrn  45947  icccncfext  46621  stoweidlem29  46763  stoweidlem31  46765  stoweidlem59  46793  subsaliuncllem  47091  meadjiunlem  47199  uniimaprimaeqfv  48151  uniimaelsetpreimafv  48165