Theorem dffn2 6658

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

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3437   ⊆ wss 3898  ran crn 5620   Fn wfn 6481  ⟶wf 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-f 6490

This theorem is referenced by:  f1cnvcnv  6733  fcoconst  7073  fnressn  7097  fndifnfp  7116  1stcof  7957  2ndcof  7958  fnmpo  8007  tposfn  8191  tz7.48lem  8366  seqomlem2  8376  mptelixpg  8865  r111  9675  smobeth  10484  inar1  10673  imasvscafn  17443  fucidcl  17877  fucsect  17884  dfinito3  17914  dftermo3  17915  curfcl  18140  curf2ndf  18155  dsmmbas2  21676  frlmsslsp  21735  frlmup1  21737  prdstopn  23544  prdstps  23545  ist0-4  23645  ptuncnv  23723  xpstopnlem2  23727  prdstgpd  24041  prdsxmslem2  24445  curry2ima  32694  mplvrpmrhm  33595  onvf1od  35172  fnchoice  45150  fsneqrn  45332  stoweidlem35  46157  ixpv  49014  basresposfo  49102  fucorid2  49488  precofval2  49494