Theorem dffn3 6558

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 3923	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 533	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6384	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 281	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 209   ∧ wa 399   ⊆ wss 3866  ran crn 5552   Fn wfn 6375  ⟶wf 6376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-f 6384

This theorem is referenced by:  ffrn  6559  ffrnb  6560  fsn2  6951  offsplitfpar  7888  fo2ndf  7890  suppcoss  7949  fndmfisuppfi  8997  fndmfifsupp  8998  fin23lem17  9952  fin23lem32  9958  fnct  10151  yoniso  17793  1stckgen  22451  ovolicc2  24419  i1fadd  24592  i1fmul  24593  itg1addlem4  24596  itg1addlem4OLD  24597  i1fmulc  24601  clwlkclwwlklem2  28083  foresf1o  30569  fcoinver  30665  ofpreima2  30723  locfinreflem  31504  pl1cn  31619  fvineqsneu  35319  poimirlem29  35543  poimirlem30  35544  itg2addnclem2  35566  mapdcl  39404  wessf1ornlem  42395  unirnmap  42421  fsneqrn  42424  icccncfext  43103  stoweidlem29  43245  stoweidlem31  43247  stoweidlem59  43275  subsaliuncllem  43571  meadjiunlem  43678  uniimaprimaeqfv  44507  uniimaelsetpreimafv  44521