Theorem dffn2 6708

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

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3459   ⊆ wss 3926  ran crn 5655   Fn wfn 6526  ⟶wf 6527

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-f 6535

This theorem is referenced by:  f1cnvcnv  6783  fcoconst  7124  fnressn  7148  fndifnfp  7168  1stcof  8018  2ndcof  8019  fnmpo  8068  tposfn  8254  tz7.48lem  8455  seqomlem2  8465  mptelixpg  8949  r111  9789  smobeth  10600  inar1  10789  imasvscafn  17551  fucidcl  17981  fucsect  17988  dfinito3  18018  dftermo3  18019  curfcl  18244  curf2ndf  18259  dsmmbas2  21697  frlmsslsp  21756  frlmup1  21758  prdstopn  23566  prdstps  23567  ist0-4  23667  ptuncnv  23745  xpstopnlem2  23749  prdstgpd  24063  prdsxmslem2  24468  curry2ima  32686  fnchoice  45053  fsneqrn  45235  stoweidlem35  46064  ixpv  48865  basresposfo  48952  fucorid2  49274  precofval2  49280