Theorem dffn2 6689

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

Syntax hints:   ↔ wb 208   ∧ wa 399  Vcvv 3453   ⊆ wss 3904  ran crn 5646   Fn wfn 6512  ⟶wf 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-f 6521

This theorem is referenced by:  f1cnvcnv  6767  fcoconst  7112  fnressn  7137  fndifnfp  7156  1stcof  7996  2ndcof  7997  fnmpo  8046  tposfn  8230  tz7.48lem  8407  seqomlem2  8417  mptelixpg  8913  r111  9730  smobeth  10541  inar1  10730  imasvscafn  17550  fucidcl  17984  fucsect  17991  dfinito3  18021  dftermo3  18022  curfcl  18247  curf2ndf  18262  dsmmbas2  21769  frlmsslsp  21828  frlmup1  21830  prdstopn  23668  prdstps  23669  ist0-4  23769  ptuncnv  23847  xpstopnlem2  23851  prdstgpd  24165  prdsxmslem2  24569  curry2ima  32861  mplvrpmrhm  33805  onvf1od  35414  fnchoice  45573  fsneqrn  45751  stoweidlem35  46573  ixpv  49475  basresposfo  49563  fucorid2  49948  precofval2  49954