Theorem dffn2 6709

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

Syntax hints:   ↔ wb 209   ∧ wa 400  Vcvv 3455   ⊆ wss 3906  ran crn 5664   Fn wfn 6533  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-f 6542

This theorem is referenced by:  f1cnvcnv  6787  fcoconst  7132  fnressn  7157  fndifnfp  7176  1stcof  8017  2ndcof  8018  fnmpo  8067  tposfn  8252  tz7.48lem  8429  seqomlem2  8439  mptelixpg  8934  r111  9748  smobeth  10572  inar1  10761  imasvscafn  17592  fucidcl  18026  fucsect  18033  dfinito3  18063  dftermo3  18064  curfcl  18289  curf2ndf  18304  dsmmbas2  21868  frlmsslsp  21927  frlmup1  21929  prdstopn  23766  prdstps  23767  ist0-4  23867  ptuncnv  23945  xpstopnlem2  23949  prdstgpd  24263  prdsxmslem2  24667  curry2ima  33032  mplvrpmrhm  33915  onvf1od  35569  fnchoice  45729  fsneqrn  45907  stoweidlem35  46729  ixpv  49645  basresposfo  49733  fucorid2  50118  precofval2  50124