Theorem dffn3 6519

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ⊆ wss 3935  ran crn 5550   Fn wfn 6344  ⟶wf 6345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951  df-f 6353

This theorem is referenced by:  ffrn  6520  fsn2  6892  offsplitfpar  7809  fo2ndf  7811  fndmfisuppfi  8839  fndmfifsupp  8840  fin23lem17  9754  fin23lem32  9760  fnct  9953  yoniso  17529  1stckgen  22156  ovolicc2  24117  i1fadd  24290  i1fmul  24291  itg1addlem4  24294  i1fmulc  24298  clwlkclwwlklem2  27772  foresf1o  30259  fcoinver  30351  ofpreima2  30405  locfinreflem  31099  pl1cn  31193  fvineqsneu  34686  poimirlem29  34915  poimirlem30  34916  itg2addnclem2  34938  mapdcl  38783  wessf1ornlem  41438  unirnmap  41464  fsneqrn  41467  icccncfext  42163  stoweidlem29  42308  stoweidlem31  42310  stoweidlem59  42338  subsaliuncllem  42634  meadjiunlem  42741  uniimaprimaeqfv  43536  uniimaelsetpreimafv  43550