Theorem dffn2 6719

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

Syntax hints:   ↔ wb 205   ∧ wa 396  Vcvv 3474   ⊆ wss 3948  ran crn 5677   Fn wfn 6538  ⟶wf 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-f 6547

This theorem is referenced by:  f1cnvcnv  6797  fcoconst  7134  fnressn  7158  fndifnfp  7176  1stcof  8007  2ndcof  8008  fnmpo  8057  tposfn  8242  tz7.48lem  8443  seqomlem2  8453  mptelixpg  8931  r111  9772  smobeth  10583  inar1  10772  imasvscafn  17487  fucidcl  17922  fucsect  17929  dfinito3  17959  dftermo3  17960  curfcl  18189  curf2ndf  18204  dsmmbas2  21511  frlmsslsp  21570  frlmup1  21572  prdstopn  23352  prdstps  23353  ist0-4  23453  ptuncnv  23531  xpstopnlem2  23535  prdstgpd  23849  prdsxmslem2  24258  curry2ima  32185  fnchoice  44015  fsneqrn  44209  stoweidlem35  45050