Theorem dffn2 6654

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

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3436   ⊆ wss 3903  ran crn 5620   Fn wfn 6477  ⟶wf 6478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-f 6486

This theorem is referenced by:  f1cnvcnv  6729  fcoconst  7068  fnressn  7092  fndifnfp  7112  1stcof  7954  2ndcof  7955  fnmpo  8004  tposfn  8188  tz7.48lem  8363  seqomlem2  8373  mptelixpg  8862  r111  9671  smobeth  10480  inar1  10669  imasvscafn  17441  fucidcl  17875  fucsect  17882  dfinito3  17912  dftermo3  17913  curfcl  18138  curf2ndf  18153  dsmmbas2  21644  frlmsslsp  21703  frlmup1  21705  prdstopn  23513  prdstps  23514  ist0-4  23614  ptuncnv  23692  xpstopnlem2  23696  prdstgpd  24010  prdsxmslem2  24415  curry2ima  32652  onvf1od  35090  fnchoice  45017  fsneqrn  45199  stoweidlem35  46026  ixpv  48884  basresposfo  48972  fucorid2  49358  precofval2  49364