Theorem dffn2 6516

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

Syntax hints:   ↔ wb 208   ∧ wa 398  Vcvv 3494   ⊆ wss 3936  ran crn 5556   Fn wfn 6350  ⟶wf 6351

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-v 3496  df-in 3943  df-ss 3952  df-f 6359

This theorem is referenced by:  f1cnvcnv  6584  fcoconst  6896  fnressn  6920  fndifnfp  6938  1stcof  7719  2ndcof  7720  fnmpo  7767  tposfn  7921  tz7.48lem  8077  seqomlem2  8087  mptelixpg  8499  r111  9204  smobeth  10008  inar1  10197  imasvscafn  16810  fucidcl  17235  fucsect  17242  curfcl  17482  curf2ndf  17497  dsmmbas2  20881  frlmsslsp  20940  frlmup1  20942  prdstopn  22236  prdstps  22237  ist0-4  22337  ptuncnv  22415  xpstopnlem2  22419  prdstgpd  22733  prdsxmslem2  23139  curry2ima  30444  fnchoice  41306  fsneqrn  41494  stoweidlem35  42340