Theorem dffn3 6716

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 3953	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 539	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6537	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 281	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ⊆ wss 3899  ran crn 5656   Fn wfn 6528  ⟶wf 6529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3916  df-f 6537

This theorem is used by:  ffrn  6717  ffrnb  6718  fsn2  7131  coof  7703  offsplitfpar  8117  fo2ndf  8119  suppcoss  8206  fndmfisuppfi  9348  fndmfifsupp  9349  fin23lem17  10341  fin23lem32  10347  fnct  10545  fnctOLD  10546  yoniso  18374  psdmplcl  22391  1stckgen  23781  ovolicc2  25751  i1fadd  25924  i1fmul  25925  itg1addlem4  25928  i1fmulc  25932  clwlkclwwlklem2  30471  foresf1o  32980  fcoinver  33078  ofpreima2  33140  fmptunsnop  33173  suppssnn0  33277  locfinreflem  34351  pl1cn  34466  fvineqsneu  38166  poimirlem29  38399  poimirlem30  38400  itg2addnclem2  38422  mapdcl  42527  aks6d1c6isolem2  43042  tfsconcatrev  44190  wessf1ornlem  46018  unirnmap  46039  fsneqrn  46042  icccncfext  46716  stoweidlem29  46858  stoweidlem31  46860  stoweidlem59  46888  subsaliuncllem  47186  meadjiunlem  47294  uniimaprimaeqfv  48283  uniimaelsetpreimafv  48297