Theorem dffn3 6749

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3963  ran crn 5690   Fn wfn 6558  ⟶wf 6559

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3980  df-f 6567

This theorem is referenced by:  ffrn  6750  ffrnb  6751  fsn2  7156  coof  7721  offsplitfpar  8143  fo2ndf  8145  suppcoss  8231  fndmfisuppfi  9415  fndmfifsupp  9416  fin23lem17  10376  fin23lem32  10382  fnct  10575  yoniso  18342  psdmplcl  22184  1stckgen  23578  ovolicc2  25571  i1fadd  25744  i1fmul  25745  itg1addlem4  25748  itg1addlem4OLD  25749  i1fmulc  25753  clwlkclwwlklem2  30029  foresf1o  32532  fcoinver  32624  ofpreima2  32683  fmptunsnop  32715  suppssnn0  32815  locfinreflem  33801  pl1cn  33916  fvineqsneu  37394  poimirlem29  37636  poimirlem30  37637  itg2addnclem2  37659  mapdcl  41636  aks6d1c6isolem2  42157  tfsconcatrev  43338  wessf1ornlem  45128  unirnmap  45151  fsneqrn  45154  icccncfext  45843  stoweidlem29  45985  stoweidlem31  45987  stoweidlem59  46015  subsaliuncllem  46313  meadjiunlem  46421  uniimaprimaeqfv  47307  uniimaelsetpreimafv  47321