Theorem dffn3 6703

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3917  ran crn 5642   Fn wfn 6509  ⟶wf 6510

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 3934  df-f 6518

This theorem is referenced by:  ffrn  6704  ffrnb  6705  fsn2  7111  coof  7680  offsplitfpar  8101  fo2ndf  8103  suppcoss  8189  fndmfisuppfi  9335  fndmfifsupp  9336  fin23lem17  10298  fin23lem32  10304  fnct  10497  yoniso  18253  psdmplcl  22056  1stckgen  23448  ovolicc2  25430  i1fadd  25603  i1fmul  25604  itg1addlem4  25607  i1fmulc  25611  clwlkclwwlklem2  29936  foresf1o  32440  fcoinver  32540  ofpreima2  32597  fmptunsnop  32630  suppssnn0  32737  locfinreflem  33837  pl1cn  33952  fvineqsneu  37406  poimirlem29  37650  poimirlem30  37651  itg2addnclem2  37673  mapdcl  41654  aks6d1c6isolem2  42170  tfsconcatrev  43344  wessf1ornlem  45186  unirnmap  45209  fsneqrn  45212  icccncfext  45892  stoweidlem29  46034  stoweidlem31  46036  stoweidlem59  46064  subsaliuncllem  46362  meadjiunlem  46470  uniimaprimaeqfv  47387  uniimaelsetpreimafv  47401