Theorem dffn2 6586

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

Syntax hints:   ↔ wb 205   ∧ wa 395  Vcvv 3422   ⊆ wss 3883  ran crn 5581   Fn wfn 6413  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-f 6422

This theorem is referenced by:  f1cnvcnv  6664  fcoconst  6988  fnressn  7012  fndifnfp  7030  1stcof  7834  2ndcof  7835  fnmpo  7882  tposfn  8042  tz7.48lem  8242  seqomlem2  8252  mptelixpg  8681  r111  9464  smobeth  10273  inar1  10462  imasvscafn  17165  fucidcl  17599  fucsect  17606  dfinito3  17636  dftermo3  17637  curfcl  17866  curf2ndf  17881  dsmmbas2  20854  frlmsslsp  20913  frlmup1  20915  prdstopn  22687  prdstps  22688  ist0-4  22788  ptuncnv  22866  xpstopnlem2  22870  prdstgpd  23184  prdsxmslem2  23591  curry2ima  30943  fnchoice  42461  fsneqrn  42640  stoweidlem35  43466