Theorem dffn3 6682

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3903  ran crn 5633   Fn wfn 6495  ⟶wf 6496

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3920  df-f 6504

This theorem is referenced by:  ffrn  6683  ffrnb  6684  fsn2  7091  coof  7656  offsplitfpar  8071  fo2ndf  8073  suppcoss  8159  fndmfisuppfi  9292  fndmfifsupp  9293  fin23lem17  10260  fin23lem32  10266  fnct  10459  yoniso  18220  psdmplcl  22117  1stckgen  23510  ovolicc2  25491  i1fadd  25664  i1fmul  25665  itg1addlem4  25668  i1fmulc  25672  clwlkclwwlklem2  30087  foresf1o  32591  fcoinver  32691  ofpreima2  32756  fmptunsnop  32790  suppssnn0  32896  locfinreflem  34018  pl1cn  34133  fvineqsneu  37666  poimirlem29  37900  poimirlem30  37901  itg2addnclem2  37923  mapdcl  42029  aks6d1c6isolem2  42545  tfsconcatrev  43705  wessf1ornlem  45544  unirnmap  45566  fsneqrn  45569  icccncfext  46245  stoweidlem29  46387  stoweidlem31  46389  stoweidlem59  46417  subsaliuncllem  46715  meadjiunlem  46823  uniimaprimaeqfv  47742  uniimaelsetpreimafv  47756