Theorem dffn2 6711

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  Vcvv 3450   ⊆ wss 3895  ran crn 5651   Fn wfn 6533  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-f 6542

This theorem is used by:  f1cnvcnv  6789  fcoconst  7135  fnressn  7162  fndifnfp  7181  1stcof  8031  2ndcof  8032  fnmpo  8080  tposfn  8275  tz7.48lem  8453  tz7.48lemOLD  8454  seqomlem2  8464  mptelixpg  8966  r111  9785  smobeth  10674  inar1  10863  imasvscafn  17714  fucidcl  18148  fucsect  18155  dfinito3  18185  dftermo3  18186  curfcl  18411  curf2ndf  18426  dsmmbas2  22048  frlmsslsp  22107  frlmup1  22109  prdstopn  23952  prdstps  23953  ist0-4  24053  ptuncnv  24131  xpstopnlem2  24135  prdstgpd  24449  prdsxmslem2  24853  curry2ima  33349  mplvrpmrhm  34225  acwer1prc  35816  onvf1od  35954  fnchoice  46139  fsneqrn  46317  stoweidlem35  47138  ixpv  50096  basresposfo  50185  fucorid2  50578  fucoridid  50579  precofval2  50597