Theorem dffn2 6670

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 529	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 6502	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 278	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3429   ⊆ wss 3889  ran crn 5632   Fn wfn 6493  ⟶wf 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-f 6502

This theorem is referenced by:  f1cnvcnv  6745  fcoconst  7087  fnressn  7112  fndifnfp  7131  1stcof  7972  2ndcof  7973  fnmpo  8022  tposfn  8205  tz7.48lem  8380  seqomlem2  8390  mptelixpg  8883  r111  9699  smobeth  10509  inar1  10698  imasvscafn  17501  fucidcl  17935  fucsect  17942  dfinito3  17972  dftermo3  17973  curfcl  18198  curf2ndf  18213  dsmmbas2  21717  frlmsslsp  21776  frlmup1  21778  prdstopn  23593  prdstps  23594  ist0-4  23694  ptuncnv  23772  xpstopnlem2  23776  prdstgpd  24090  prdsxmslem2  24494  curry2ima  32782  mplvrpmrhm  33691  onvf1od  35289  fnchoice  45460  fsneqrn  45640  stoweidlem35  46463  ixpv  49365  basresposfo  49453  fucorid2  49838  precofval2  49844