Theorem dffn2 6697

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 3963	. . 3 ⊢ ran 𝐹 ⊆ V
2	1	biantru 538	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 6529	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 281	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 209   ∧ wa 400  Vcvv 3457   ⊆ wss 3907  ran crn 5652   Fn wfn 6520  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-f 6529

This theorem is referenced by:  f1cnvcnv  6775  fcoconst  7120  fnressn  7145  fndifnfp  7164  1stcof  8004  2ndcof  8005  fnmpo  8054  tposfn  8239  tz7.48lem  8416  seqomlem2  8426  mptelixpg  8921  r111  9735  smobeth  10559  inar1  10748  imasvscafn  17579  fucidcl  18013  fucsect  18020  dfinito3  18050  dftermo3  18051  curfcl  18276  curf2ndf  18291  dsmmbas2  21844  frlmsslsp  21903  frlmup1  21905  prdstopn  23742  prdstps  23743  ist0-4  23843  ptuncnv  23921  xpstopnlem2  23925  prdstgpd  24239  prdsxmslem2  24643  curry2ima  32962  mplvrpmrhm  33849  onvf1od  35457  fnchoice  45608  fsneqrn  45786  stoweidlem35  46608  ixpv  49520  basresposfo  49608  fucorid2  49993  precofval2  49999