Theorem dffn2 6518

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 3993	. . 3 ⊢ ran 𝐹 ⊆ V
2	1	biantru 532	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 6361	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 280	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 208   ∧ wa 398  Vcvv 3496   ⊆ wss 3938  ran crn 5558   Fn wfn 6352  ⟶wf 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-v 3498  df-in 3945  df-ss 3954  df-f 6361

This theorem is referenced by:  f1cnvcnv  6586  fcoconst  6898  fnressn  6922  fndifnfp  6940  1stcof  7721  2ndcof  7722  fnmpo  7769  tposfn  7923  tz7.48lem  8079  seqomlem2  8089  mptelixpg  8501  r111  9206  smobeth  10010  inar1  10199  imasvscafn  16812  fucidcl  17237  fucsect  17244  curfcl  17484  curf2ndf  17499  dsmmbas2  20883  frlmsslsp  20942  frlmup1  20944  prdstopn  22238  prdstps  22239  ist0-4  22339  ptuncnv  22417  xpstopnlem2  22421  prdstgpd  22735  prdsxmslem2  23141  curry2ima  30446  fnchoice  41293  fsneqrn  41481  stoweidlem35  42327