Theorem dffn2 6525

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 3911	. . 3 ⊢ ran 𝐹 ⊆ V
2	1	biantru 533	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 6362	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 281	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 209   ∧ wa 399  Vcvv 3398   ⊆ wss 3853  ran crn 5537   Fn wfn 6353  ⟶wf 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-f 6362

This theorem is referenced by:  f1cnvcnv  6603  fcoconst  6927  fnressn  6951  fndifnfp  6969  1stcof  7769  2ndcof  7770  fnmpo  7817  tposfn  7975  tz7.48lem  8155  seqomlem2  8165  mptelixpg  8594  r111  9356  smobeth  10165  inar1  10354  imasvscafn  16996  fucidcl  17428  fucsect  17435  dfinito3  17465  dftermo3  17466  curfcl  17694  curf2ndf  17709  dsmmbas2  20653  frlmsslsp  20712  frlmup1  20714  prdstopn  22479  prdstps  22480  ist0-4  22580  ptuncnv  22658  xpstopnlem2  22662  prdstgpd  22976  prdsxmslem2  23381  curry2ima  30715  fnchoice  42186  fsneqrn  42365  stoweidlem35  43194