Theorem dffn3 6718

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3926  ran crn 5655   Fn wfn 6526  ⟶wf 6527

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3943  df-f 6535

This theorem is referenced by:  ffrn  6719  ffrnb  6720  fsn2  7126  coof  7695  offsplitfpar  8118  fo2ndf  8120  suppcoss  8206  fndmfisuppfi  9389  fndmfifsupp  9390  fin23lem17  10352  fin23lem32  10358  fnct  10551  yoniso  18297  psdmplcl  22100  1stckgen  23492  ovolicc2  25475  i1fadd  25648  i1fmul  25649  itg1addlem4  25652  i1fmulc  25656  clwlkclwwlklem2  29981  foresf1o  32485  fcoinver  32585  ofpreima2  32644  fmptunsnop  32677  suppssnn0  32784  locfinreflem  33871  pl1cn  33986  fvineqsneu  37429  poimirlem29  37673  poimirlem30  37674  itg2addnclem2  37696  mapdcl  41672  aks6d1c6isolem2  42188  tfsconcatrev  43372  wessf1ornlem  45209  unirnmap  45232  fsneqrn  45235  icccncfext  45916  stoweidlem29  46058  stoweidlem31  46060  stoweidlem59  46088  subsaliuncllem  46386  meadjiunlem  46494  uniimaprimaeqfv  47396  uniimaelsetpreimafv  47410