Theorem dffn3 6207

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 3757	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 527	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6045	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 267	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 196   ∧ wa 383   ⊆ wss 3707  ran crn 5259   Fn wfn 6036  ⟶wf 6037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-in 3714  df-ss 3721  df-f 6045

This theorem is referenced by:  ffrn  6208  fsn2  6558  fo2ndf  7444  fndmfisuppfi  8444  fndmfifsupp  8445  fin23lem17  9344  fin23lem32  9350  fnct  9543  yoniso  17118  1stckgen  21551  ovolicc2  23482  itg1val2  23642  i1fadd  23653  i1fmul  23654  itg1addlem4  23657  i1fmulc  23661  clwlkclwwlklem2  27115  foresf1o  29642  fcoinver  29717  ofpreima2  29767  locfinreflem  30208  pl1cn  30302  poimirlem29  33743  poimirlem30  33744  itg2addnclem2  33767  mapdcl  37436  wessf1ornlem  39862  unirnmap  39891  fsneqrn  39894  icccncfext  40595  stoweidlem29  40741  stoweidlem31  40743  stoweidlem59  40771  subsaliuncllem  41070  meadjiunlem  41177