Theorem dffn2 6714

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  Vcvv 3458   ⊆ wss 3908  ran crn 5667   Fn wfn 6538  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-f 6547

This theorem is used by:  f1cnvcnv  6792  fcoconst  7137  fnressn  7162  fndifnfp  7181  1stcof  8025  2ndcof  8026  fnmpo  8075  tposfn  8260  tz7.48lem  8437  seqomlem2  8447  mptelixpg  8942  r111  9757  smobeth  10589  inar1  10778  imasvscafn  17616  fucidcl  18050  fucsect  18057  dfinito3  18087  dftermo3  18088  curfcl  18313  curf2ndf  18328  dsmmbas2  21924  frlmsslsp  21983  frlmup1  21985  prdstopn  23822  prdstps  23823  ist0-4  23923  ptuncnv  24001  xpstopnlem2  24005  prdstgpd  24319  prdsxmslem2  24723  curry2ima  33091  mplvrpmrhm  33968  onvf1od  35615  fnchoice  45790  fsneqrn  45968  stoweidlem35  46790  ixpv  49709  basresposfo  49797  fucorid2  50182  precofval2  50188