Theorem dffn3 6658

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3899  ran crn 5614   Fn wfn 6471  ⟶wf 6472

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 3916  df-f 6480

This theorem is referenced by:  ffrn  6659  ffrnb  6660  fsn2  7063  coof  7628  offsplitfpar  8043  fo2ndf  8045  suppcoss  8131  fndmfisuppfi  9255  fndmfifsupp  9256  fin23lem17  10220  fin23lem32  10226  fnct  10419  yoniso  18178  psdmplcl  22031  1stckgen  23423  ovolicc2  25404  i1fadd  25577  i1fmul  25578  itg1addlem4  25581  i1fmulc  25585  clwlkclwwlklem2  29931  foresf1o  32436  fcoinver  32536  ofpreima2  32600  fmptunsnop  32633  suppssnn0  32742  locfinreflem  33821  pl1cn  33936  fvineqsneu  37402  poimirlem29  37646  poimirlem30  37647  itg2addnclem2  37669  mapdcl  41649  aks6d1c6isolem2  42165  tfsconcatrev  43338  wessf1ornlem  45179  unirnmap  45202  fsneqrn  45205  icccncfext  45882  stoweidlem29  46024  stoweidlem31  46026  stoweidlem59  46054  subsaliuncllem  46352  meadjiunlem  46460  uniimaprimaeqfv  47380  uniimaelsetpreimafv  47394