Theorem dffn3 6622

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 3944	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 530	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6441	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 277	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 205   ∧ wa 396   ⊆ wss 3888  ran crn 5591   Fn wfn 6432  ⟶wf 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-f 6441

This theorem is referenced by:  ffrn  6623  ffrnb  6624  fsn2  7017  offsplitfpar  7969  fo2ndf  7971  suppcoss  8032  fndmfisuppfi  9149  fndmfifsupp  9150  fin23lem17  10103  fin23lem32  10109  fnct  10302  yoniso  18012  1stckgen  22714  ovolicc2  24695  i1fadd  24868  i1fmul  24869  itg1addlem4  24872  itg1addlem4OLD  24873  i1fmulc  24877  clwlkclwwlklem2  28373  foresf1o  30859  fcoinver  30955  ofpreima2  31012  locfinreflem  31799  pl1cn  31914  fvineqsneu  35591  poimirlem29  35815  poimirlem30  35816  itg2addnclem2  35838  mapdcl  39674  wessf1ornlem  42729  unirnmap  42755  fsneqrn  42758  icccncfext  43435  stoweidlem29  43577  stoweidlem31  43579  stoweidlem59  43607  subsaliuncllem  43903  meadjiunlem  44010  uniimaprimaeqfv  44845  uniimaelsetpreimafv  44859