Theorem dffn2 6690

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

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3447   ⊆ wss 3914  ran crn 5639   Fn wfn 6506  ⟶wf 6507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-f 6515

This theorem is referenced by:  f1cnvcnv  6765  fcoconst  7106  fnressn  7130  fndifnfp  7150  1stcof  7998  2ndcof  7999  fnmpo  8048  tposfn  8234  tz7.48lem  8409  seqomlem2  8419  mptelixpg  8908  r111  9728  smobeth  10539  inar1  10728  imasvscafn  17500  fucidcl  17930  fucsect  17937  dfinito3  17967  dftermo3  17968  curfcl  18193  curf2ndf  18208  dsmmbas2  21646  frlmsslsp  21705  frlmup1  21707  prdstopn  23515  prdstps  23516  ist0-4  23616  ptuncnv  23694  xpstopnlem2  23698  prdstgpd  24012  prdsxmslem2  24417  curry2ima  32632  onvf1od  35094  fnchoice  45023  fsneqrn  45205  stoweidlem35  46033  ixpv  48878  basresposfo  48966  fucorid2  49352  precofval2  49358