Theorem dffn2 6653

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

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3436   ⊆ wss 3902  ran crn 5617   Fn wfn 6476  ⟶wf 6477

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-f 6485

This theorem is referenced by:  f1cnvcnv  6728  fcoconst  7067  fnressn  7091  fndifnfp  7110  1stcof  7951  2ndcof  7952  fnmpo  8001  tposfn  8185  tz7.48lem  8360  seqomlem2  8370  mptelixpg  8859  r111  9665  smobeth  10474  inar1  10663  imasvscafn  17438  fucidcl  17872  fucsect  17879  dfinito3  17909  dftermo3  17910  curfcl  18135  curf2ndf  18150  dsmmbas2  21672  frlmsslsp  21731  frlmup1  21733  prdstopn  23541  prdstps  23542  ist0-4  23642  ptuncnv  23720  xpstopnlem2  23724  prdstgpd  24038  prdsxmslem2  24442  curry2ima  32685  mplvrpmrhm  33572  onvf1od  35139  fnchoice  45065  fsneqrn  45247  stoweidlem35  46072  ixpv  48920  basresposfo  49008  fucorid2  49394  precofval2  49400