Theorem dffn2 6716

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

Syntax hints:   ↔ wb 205   ∧ wa 396  Vcvv 3474   ⊆ wss 3947  ran crn 5676   Fn wfn 6535  ⟶wf 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-f 6544

This theorem is referenced by:  f1cnvcnv  6794  fcoconst  7128  fnressn  7152  fndifnfp  7170  1stcof  8001  2ndcof  8002  fnmpo  8051  tposfn  8236  tz7.48lem  8437  seqomlem2  8447  mptelixpg  8925  r111  9766  smobeth  10577  inar1  10766  imasvscafn  17479  fucidcl  17914  fucsect  17921  dfinito3  17951  dftermo3  17952  curfcl  18181  curf2ndf  18196  dsmmbas2  21283  frlmsslsp  21342  frlmup1  21344  prdstopn  23123  prdstps  23124  ist0-4  23224  ptuncnv  23302  xpstopnlem2  23306  prdstgpd  23620  prdsxmslem2  24029  curry2ima  31917  fnchoice  43698  fsneqrn  43895  stoweidlem35  44737