Theorem dffn3 6722

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ⊆ wss 3906  ran crn 5664   Fn wfn 6535  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3923  df-f 6544

This theorem is used by:  ffrn  6723  ffrnb  6724  fsn2  7136  coof  7708  offsplitfpar  8120  fo2ndf  8122  suppcoss  8209  fndmfisuppfi  9344  fndmfifsupp  9345  fin23lem17  10337  fin23lem32  10343  fnct  10538  yoniso  18365  psdmplcl  22377  1stckgen  23764  ovolicc2  25734  i1fadd  25907  i1fmul  25908  itg1addlem4  25911  i1fmulc  25915  clwlkclwwlklem2  30420  foresf1o  32923  fcoinver  33022  ofpreima2  33084  fmptunsnop  33118  suppssnn0  33222  locfinreflem  34296  pl1cn  34411  fvineqsneu  38116  poimirlem29  38359  poimirlem30  38360  itg2addnclem2  38382  mapdcl  42487  aks6d1c6isolem2  43002  tfsconcatrev  44135  wessf1ornlem  45963  unirnmap  45984  fsneqrn  45987  icccncfext  46661  stoweidlem29  46803  stoweidlem31  46805  stoweidlem59  46833  subsaliuncllem  47131  meadjiunlem  47239  uniimaprimaeqfv  48191  uniimaelsetpreimafv  48205