Theorem dffn2 6658

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 3962	. . 3 ⊢ ran 𝐹 ⊆ V
2	1	biantru 529	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 6490	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 278	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3438   ⊆ wss 3905  ran crn 5624   Fn wfn 6481  ⟶wf 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-f 6490

This theorem is referenced by:  f1cnvcnv  6733  fcoconst  7072  fnressn  7096  fndifnfp  7116  1stcof  7961  2ndcof  7962  fnmpo  8011  tposfn  8195  tz7.48lem  8370  seqomlem2  8380  mptelixpg  8869  r111  9690  smobeth  10499  inar1  10688  imasvscafn  17459  fucidcl  17893  fucsect  17900  dfinito3  17930  dftermo3  17931  curfcl  18156  curf2ndf  18171  dsmmbas2  21662  frlmsslsp  21721  frlmup1  21723  prdstopn  23531  prdstps  23532  ist0-4  23632  ptuncnv  23710  xpstopnlem2  23714  prdstgpd  24028  prdsxmslem2  24433  curry2ima  32665  onvf1od  35079  fnchoice  45007  fsneqrn  45189  stoweidlem35  46017  ixpv  48875  basresposfo  48963  fucorid2  49349  precofval2  49355