Theorem dffn3 6728

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ⊆ wss 3948  ran crn 5677   Fn wfn 6536  ⟶wf 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-f 6545

This theorem is referenced by:  ffrn  6729  ffrnb  6730  fsn2  7131  offsplitfpar  8102  fo2ndf  8104  suppcoss  8189  fndmfisuppfi  9372  fndmfifsupp  9373  fin23lem17  10330  fin23lem32  10336  fnct  10529  yoniso  18235  1stckgen  23050  ovolicc2  25031  i1fadd  25204  i1fmul  25205  itg1addlem4  25208  itg1addlem4OLD  25209  i1fmulc  25213  clwlkclwwlklem2  29243  foresf1o  31730  fcoinver  31823  ofpreima2  31879  suppssnn0  32005  locfinreflem  32809  pl1cn  32924  fvineqsneu  36281  poimirlem29  36506  poimirlem30  36507  itg2addnclem2  36529  mapdcl  40513  tfsconcatrev  42084  wessf1ornlem  43868  unirnmap  43893  fsneqrn  43896  icccncfext  44590  stoweidlem29  44732  stoweidlem31  44734  stoweidlem59  44762  subsaliuncllem  45060  meadjiunlem  45168  uniimaprimaeqfv  46037  uniimaelsetpreimafv  46051