Theorem dffn3 6730

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 3934	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 539	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6550	. 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 5655   Fn wfn 6541  ⟶wf 6542

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3900  df-f 6550

This theorem is used by:  ffrn  6731  ffrnb  6732  fsn2  7145  coof  7724  offsplitfpar  8140  fo2ndf  8142  suppcoss  8235  fndmfisuppfi  9379  fndmfifsupp  9380  fin23lem17  10426  fin23lem32  10432  fnct  10630  fnctOLD  10631  yoniso  18471  psdmplcl  22495  1stckgen  23885  ovolicc2  25855  i1fadd  26028  i1fmul  26029  itg1addlem4  26032  i1fmulc  26036  clwlkclwwlklem2  30603  foresf1o  33154  fcoinver  33252  ofpreima2  33314  fmptunsnop  33347  suppssnn0  33450  locfinreflem  34525  pl1cn  34640  rncardr1prc  35829  fvineqsneu  38474  poimirlem29  38707  poimirlem30  38708  itg2addnclem2  38730  mapdcl  42850  aks6d1c6isolem2  43365  tfsconcatrev  44490  wessf1ornlem  46339  unirnmap  46360  fsneqrn  46363  icccncfext  47036  stoweidlem29  47178  stoweidlem31  47180  stoweidlem59  47208  subsaliuncllem  47506  meadjiunlem  47614  uniimaprimaeqfv  48603  uniimaelsetpreimafv  48617