Theorem dffn2 6664

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 3946	. . 3 ⊢ ran 𝐹 ⊆ V
2	1	biantru 534	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 6496	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 279	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 207   ∧ wa 396  Vcvv 3432   ⊆ wss 3890  ran crn 5626   Fn wfn 6487  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-f 6496

This theorem is referenced by:  f1cnvcnv  6739  fcoconst  7083  fnressn  7108  fndifnfp  7127  1stcof  7968  2ndcof  7969  fnmpo  8018  tposfn  8202  tz7.48lem  8377  seqomlem2  8387  mptelixpg  8880  r111  9697  smobeth  10507  inar1  10696  imasvscafn  17499  fucidcl  17933  fucsect  17940  dfinito3  17970  dftermo3  17971  curfcl  18196  curf2ndf  18211  dsmmbas2  21719  frlmsslsp  21778  frlmup1  21780  prdstopn  23618  prdstps  23619  ist0-4  23719  ptuncnv  23797  xpstopnlem2  23801  prdstgpd  24115  prdsxmslem2  24519  curry2ima  32808  mplvrpmrhm  33738  onvf1od  35342  fnchoice  45484  fsneqrn  45663  stoweidlem35  46485  ixpv  49387  basresposfo  49475  fucorid2  49860  precofval2  49866