Theorem dffn3 6752

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ⊆ wss 3900  ran crn 5659   Fn wfn 6561  ⟶wf 6562

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 3901  df-f 6570

This theorem is used by:  ffrn  6753  ffrnb  6754  fsn2  7169  coof  7749  offsplitfpar  8167  fo2ndf  8169  suppcoss  8262  fndmfisuppfi  9406  fndmfifsupp  9407  fin23lem17  10455  fin23lem32  10461  fnct  10659  fnctOLD  10660  yoniso  18509  psdmplcl  22538  1stckgen  23928  ovolicc2  25898  i1fadd  26071  i1fmul  26072  itg1addlem4  26075  i1fmulc  26079  clwlkclwwlklem2  30648  foresf1o  33199  fcoinver  33296  ofpreima2  33358  fmptunsnop  33390  suppssnn0  33493  locfinreflem  34583  pl1cn  34698  rncardr1prc  35891  fvineqsneu  38602  poimirlem29  38835  poimirlem30  38836  itg2addnclem2  38858  mapdcl  42976  aks6d1c6isolem2  43491  tfsconcatrev  44611  wessf1ornlem  46473  unirnmap  46494  fsneqrn  46497  icccncfext  47170  stoweidlem29  47312  stoweidlem31  47314  stoweidlem59  47342  subsaliuncllem  47640  meadjiunlem  47748  uniimaprimaeqfv  48737  uniimaelsetpreimafv  48751