Theorem dffn3 6722

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 6542	. 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 5652   Fn wfn 6533  ⟶wf 6534

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 6542

This theorem is used by:  ffrn  6723  ffrnb  6724  fsn2  7137  coof  7717  offsplitfpar  8130  fo2ndf  8132  suppcoss  8224  fndmfisuppfi  9369  fndmfifsupp  9370  fin23lem17  10416  fin23lem32  10422  fnct  10620  fnctOLD  10621  yoniso  18459  psdmplcl  22483  1stckgen  23873  ovolicc2  25843  i1fadd  26016  i1fmul  26017  itg1addlem4  26020  i1fmulc  26024  clwlkclwwlklem2  30591  foresf1o  33100  fcoinver  33198  ofpreima2  33260  fmptunsnop  33293  suppssnn0  33397  locfinreflem  34472  pl1cn  34587  rncardr1prc  35758  fvineqsneu  38334  poimirlem29  38567  poimirlem30  38568  itg2addnclem2  38590  mapdcl  42710  aks6d1c6isolem2  43225  tfsconcatrev  44349  wessf1ornlem  46199  unirnmap  46220  fsneqrn  46223  icccncfext  46896  stoweidlem29  47038  stoweidlem31  47040  stoweidlem59  47068  subsaliuncllem  47366  meadjiunlem  47474  uniimaprimaeqfv  48463  uniimaelsetpreimafv  48477