Theorem dffn3 6674

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3901  ran crn 5625   Fn wfn 6487  ⟶wf 6488

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3918  df-f 6496

This theorem is referenced by:  ffrn  6675  ffrnb  6676  fsn2  7081  coof  7646  offsplitfpar  8061  fo2ndf  8063  suppcoss  8149  fndmfisuppfi  9280  fndmfifsupp  9281  fin23lem17  10248  fin23lem32  10254  fnct  10447  yoniso  18208  psdmplcl  22105  1stckgen  23498  ovolicc2  25479  i1fadd  25652  i1fmul  25653  itg1addlem4  25656  i1fmulc  25660  clwlkclwwlklem2  30075  foresf1o  32579  fcoinver  32679  ofpreima2  32744  fmptunsnop  32779  suppssnn0  32885  locfinreflem  33997  pl1cn  34112  fvineqsneu  37616  poimirlem29  37850  poimirlem30  37851  itg2addnclem2  37873  mapdcl  41913  aks6d1c6isolem2  42429  tfsconcatrev  43590  wessf1ornlem  45429  unirnmap  45452  fsneqrn  45455  icccncfext  46131  stoweidlem29  46273  stoweidlem31  46275  stoweidlem59  46303  subsaliuncllem  46601  meadjiunlem  46709  uniimaprimaeqfv  47628  uniimaelsetpreimafv  47642