Theorem dffn3 6700

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3914  ran crn 5639   Fn wfn 6506  ⟶wf 6507

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 3931  df-f 6515

This theorem is referenced by:  ffrn  6701  ffrnb  6702  fsn2  7108  coof  7677  offsplitfpar  8098  fo2ndf  8100  suppcoss  8186  fndmfisuppfi  9328  fndmfifsupp  9329  fin23lem17  10291  fin23lem32  10297  fnct  10490  yoniso  18246  psdmplcl  22049  1stckgen  23441  ovolicc2  25423  i1fadd  25596  i1fmul  25597  itg1addlem4  25600  i1fmulc  25604  clwlkclwwlklem2  29929  foresf1o  32433  fcoinver  32533  ofpreima2  32590  fmptunsnop  32623  suppssnn0  32730  locfinreflem  33830  pl1cn  33945  fvineqsneu  37399  poimirlem29  37643  poimirlem30  37644  itg2addnclem2  37666  mapdcl  41647  aks6d1c6isolem2  42163  tfsconcatrev  43337  wessf1ornlem  45179  unirnmap  45202  fsneqrn  45205  icccncfext  45885  stoweidlem29  46027  stoweidlem31  46029  stoweidlem59  46057  subsaliuncllem  46355  meadjiunlem  46463  uniimaprimaeqfv  47383  uniimaelsetpreimafv  47397