Theorem dffn3 6704

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 3958	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 537	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6525	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 280	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 208   ∧ wa 399   ⊆ wss 3904  ran crn 5648   Fn wfn 6516  ⟶wf 6517

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ss 3921  df-f 6525

This theorem is referenced by:  ffrn  6705  ffrnb  6706  fsn2  7118  coof  7684  offsplitfpar  8098  fo2ndf  8100  suppcoss  8187  fndmfisuppfi  9323  fndmfifsupp  9324  fin23lem17  10295  fin23lem32  10301  fnct  10494  yoniso  18317  psdmplcl  22227  1stckgen  23614  ovolicc2  25584  i1fadd  25757  i1fmul  25758  itg1addlem4  25761  i1fmulc  25765  clwlkclwwlklem2  30202  foresf1o  32703  fcoinver  32804  ofpreima2  32868  fmptunsnop  32902  suppssnn0  33007  locfinreflem  34137  pl1cn  34252  fvineqsneu  37905  poimirlem29  38148  poimirlem30  38149  itg2addnclem2  38171  mapdcl  42277  aks6d1c6isolem2  42792  tfsconcatrev  43925  wessf1ornlem  45763  unirnmap  45784  fsneqrn  45787  icccncfext  46461  stoweidlem29  46603  stoweidlem31  46605  stoweidlem59  46633  subsaliuncllem  46931  meadjiunlem  47039  uniimaprimaeqfv  47988  uniimaelsetpreimafv  48002