Theorem dffn2 6664

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 3958	. . 3 ⊢ ran 𝐹 ⊆ V
2	1	biantru 529	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 6496	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 278	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3440   ⊆ wss 3901  ran crn 5625   Fn wfn 6487  ⟶wf 6488

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-f 6496

This theorem is referenced by:  f1cnvcnv  6739  fcoconst  7079  fnressn  7103  fndifnfp  7122  1stcof  7963  2ndcof  7964  fnmpo  8013  tposfn  8197  tz7.48lem  8372  seqomlem2  8382  mptelixpg  8873  r111  9687  smobeth  10497  inar1  10686  imasvscafn  17458  fucidcl  17892  fucsect  17899  dfinito3  17929  dftermo3  17930  curfcl  18155  curf2ndf  18170  dsmmbas2  21692  frlmsslsp  21751  frlmup1  21753  prdstopn  23572  prdstps  23573  ist0-4  23673  ptuncnv  23751  xpstopnlem2  23755  prdstgpd  24069  prdsxmslem2  24473  curry2ima  32788  mplvrpmrhm  33712  onvf1od  35301  fnchoice  45270  fsneqrn  45451  stoweidlem35  46275  ixpv  49131  basresposfo  49219  fucorid2  49604  precofval2  49610