Theorem dffn2 6664

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

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3430   ⊆ wss 3890  ran crn 5625   Fn wfn 6487  ⟶wf 6488

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-f 6496

This theorem is referenced by:  f1cnvcnv  6739  fcoconst  7081  fnressn  7105  fndifnfp  7124  1stcof  7965  2ndcof  7966  fnmpo  8015  tposfn  8198  tz7.48lem  8373  seqomlem2  8383  mptelixpg  8876  r111  9690  smobeth  10500  inar1  10689  imasvscafn  17492  fucidcl  17926  fucsect  17933  dfinito3  17963  dftermo3  17964  curfcl  18189  curf2ndf  18204  dsmmbas2  21727  frlmsslsp  21786  frlmup1  21788  prdstopn  23603  prdstps  23604  ist0-4  23704  ptuncnv  23782  xpstopnlem2  23786  prdstgpd  24100  prdsxmslem2  24504  curry2ima  32797  mplvrpmrhm  33706  onvf1od  35305  fnchoice  45478  fsneqrn  45658  stoweidlem35  46481  ixpv  49377  basresposfo  49465  fucorid2  49850  precofval2  49856