Theorem dffn2 6703

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  Vcvv 3451   ⊆ wss 3899  ran crn 5652   Fn wfn 6526  ⟶wf 6527

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-f 6535

This theorem is used by:  f1cnvcnv  6781  fcoconst  7127  fnressn  7154  fndifnfp  7173  1stcof  8020  2ndcof  8021  fnmpo  8069  tposfn  8256  tz7.48lem  8434  tz7.48lemOLD  8435  seqomlem2  8445  mptelixpg  8947  r111  9765  smobeth  10652  inar1  10841  imasvscafn  17689  fucidcl  18123  fucsect  18130  dfinito3  18160  dftermo3  18161  curfcl  18386  curf2ndf  18401  dsmmbas2  22023  frlmsslsp  22082  frlmup1  22084  prdstopn  23927  prdstps  23928  ist0-4  24028  ptuncnv  24106  xpstopnlem2  24110  prdstgpd  24424  prdsxmslem2  24828  curry2ima  33284  mplvrpmrhm  34161  onvf1od  35859  fnchoice  45989  fsneqrn  46167  stoweidlem35  46989  ixpv  49942  basresposfo  50030  fucorid2  50415  precofval2  50421