Theorem dffn2 6258

Description: Any function is a mapping into V. (Contributed by NM, 31-Oct-1995.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Assertion

Ref	Expression
dffn2	⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Proof of Theorem dffn2

Step	Hyp	Ref	Expression
1		ssv 3822	. . 3 ⊢ ran 𝐹 ⊆ V
2	1	biantru 521	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 6105	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 269	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 197   ∧ wa 384  Vcvv 3391   ⊆ wss 3769  ran crn 5312   Fn wfn 6096  ⟶wf 6097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-v 3393  df-in 3776  df-ss 3783  df-f 6105

This theorem is referenced by:  f1cnvcnv  6325  fcoconst  6624  fnressn  6649  fndifnfp  6667  1stcof  7428  2ndcof  7429  fnmpt2  7471  tposfn  7616  tz7.48lem  7772  seqomlem2  7782  mptelixpg  8182  r111  8885  smobeth  9693  inar1  9882  imasvscafn  16402  fucidcl  16829  fucsect  16836  curfcl  17077  curf2ndf  17092  dsmmbas2  20291  frlmsslsp  20345  frlmup1  20347  prdstopn  21645  prdstps  21646  ist0-4  21746  ptuncnv  21824  xpstopnlem2  21828  prdstgpd  22141  prdsxmslem2  22547  curry2ima  29813  fnchoice  39682  fsneqrn  39890  stoweidlem35  40731