Theorem dffn3 5967

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 3587	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 525	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 5808	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 266	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 195   ∧ wa 383   ⊆ wss 3540  ran crn 5039   Fn wfn 5799  ⟶wf 5800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5808

This theorem is referenced by:  ffrn  5968  fsn2  6309  fo2ndf  7171  fndmfisuppfi  8170  fndmfifsupp  8171  fin23lem17  9043  fin23lem32  9049  yoniso  16748  1stckgen  21167  ovolicc2  23097  itg1val2  23257  i1fadd  23268  i1fmul  23269  itg1addlem4  23272  i1fmulc  23276  frgrancvvdeqlemB  26565  foresf1o  28727  fcoinver  28798  ofpreima2  28849  fnct  28876  locfinreflem  29235  pl1cn  29329  poimirlem29  32608  poimirlem30  32609  itg2addnclem2  32632  mapdcl  35960  wessf1ornlem  38366  unirnmap  38395  fsneqrn  38398  icccncfext  38773  stoweidlem29  38922  stoweidlem31  38924  stoweidlem59  38952  subsaliuncllem  39251  meadjiunlem  39358  clwlkclwwlklem2  41209