Theorem dffn2 6708

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  Vcvv 3453   ⊆ wss 3902  ran crn 5660   Fn wfn 6532  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-f 6541

This theorem is used by:  f1cnvcnv  6786  fcoconst  7132  fnressn  7159  fndifnfp  7178  1stcof  8020  2ndcof  8021  fnmpo  8070  tposfn  8257  tz7.48lem  8434  seqomlem2  8444  mptelixpg  8946  r111  9761  smobeth  10599  inar1  10788  imasvscafn  17629  fucidcl  18063  fucsect  18070  dfinito3  18100  dftermo3  18101  curfcl  18326  curf2ndf  18341  dsmmbas2  21956  frlmsslsp  22015  frlmup1  22017  prdstopn  23860  prdstps  23861  ist0-4  23961  ptuncnv  24039  xpstopnlem2  24043  prdstgpd  24357  prdsxmslem2  24761  curry2ima  33189  mplvrpmrhm  34065  onvf1od  35712  fnchoice  45871  fsneqrn  46049  stoweidlem35  46871  ixpv  49824  basresposfo  49912  fucorid2  50297  precofval2  50303