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 5653   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  17581  fucidcl  18015  fucsect  18022  dfinito3  18052  dftermo3  18053  curfcl  18278  curf2ndf  18293  dsmmbas2  21847  frlmsslsp  21906  frlmup1  21908  prdstopn  23746  prdstps  23747  ist0-4  23847  ptuncnv  23925  xpstopnlem2  23929  prdstgpd  24243  prdsxmslem2  24647  curry2ima  32966  mplvrpmrhm  33854  onvf1od  35462  fnchoice  45607  fsneqrn  45785  stoweidlem35  46607  ixpv  49519  basresposfo  49607  fucorid2  49992  precofval2  49998