Theorem dffn3 6658

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3897  ran crn 5612   Fn wfn 6471  ⟶wf 6472

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3914  df-f 6480

This theorem is referenced by:  ffrn  6659  ffrnb  6660  fsn2  7064  coof  7629  offsplitfpar  8044  fo2ndf  8046  suppcoss  8132  fndmfisuppfi  9256  fndmfifsupp  9257  fin23lem17  10224  fin23lem32  10230  fnct  10423  yoniso  18186  psdmplcl  22072  1stckgen  23464  ovolicc2  25445  i1fadd  25618  i1fmul  25619  itg1addlem4  25622  i1fmulc  25626  clwlkclwwlklem2  29972  foresf1o  32476  fcoinver  32576  ofpreima2  32640  fmptunsnop  32673  suppssnn0  32779  locfinreflem  33845  pl1cn  33960  fvineqsneu  37445  poimirlem29  37689  poimirlem30  37690  itg2addnclem2  37712  mapdcl  41692  aks6d1c6isolem2  42208  tfsconcatrev  43381  wessf1ornlem  45222  unirnmap  45245  fsneqrn  45248  icccncfext  45925  stoweidlem29  46067  stoweidlem31  46069  stoweidlem59  46097  subsaliuncllem  46395  meadjiunlem  46503  uniimaprimaeqfv  47413  uniimaelsetpreimafv  47427