Theorem dffn3 6525

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 3989	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 532	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6359	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 280	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 208   ∧ wa 398   ⊆ wss 3936  ran crn 5556   Fn wfn 6350  ⟶wf 6351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-f 6359

This theorem is referenced by:  ffrn  6526  fsn2  6898  offsplitfpar  7815  fo2ndf  7817  fndmfisuppfi  8845  fndmfifsupp  8846  fin23lem17  9760  fin23lem32  9766  fnct  9959  yoniso  17535  1stckgen  22162  ovolicc2  24123  i1fadd  24296  i1fmul  24297  itg1addlem4  24300  i1fmulc  24304  clwlkclwwlklem2  27778  foresf1o  30265  fcoinver  30357  ofpreima2  30411  locfinreflem  31104  pl1cn  31198  fvineqsneu  34695  poimirlem29  34936  poimirlem30  34937  itg2addnclem2  34959  mapdcl  38804  wessf1ornlem  41465  unirnmap  41491  fsneqrn  41494  icccncfext  42190  stoweidlem29  42334  stoweidlem31  42336  stoweidlem59  42364  subsaliuncllem  42660  meadjiunlem  42767  uniimaprimaeqfv  43562  uniimaelsetpreimafv  43576