Theorem dffn2 6739

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

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3478   ⊆ wss 3963  ran crn 5690   Fn wfn 6558  ⟶wf 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-f 6567

This theorem is referenced by:  f1cnvcnv  6814  fcoconst  7154  fnressn  7178  fndifnfp  7196  1stcof  8043  2ndcof  8044  fnmpo  8093  tposfn  8279  tz7.48lem  8480  seqomlem2  8490  mptelixpg  8974  r111  9813  smobeth  10624  inar1  10813  imasvscafn  17584  fucidcl  18022  fucsect  18029  dfinito3  18059  dftermo3  18060  curfcl  18289  curf2ndf  18304  dsmmbas2  21775  frlmsslsp  21834  frlmup1  21836  prdstopn  23652  prdstps  23653  ist0-4  23753  ptuncnv  23831  xpstopnlem2  23835  prdstgpd  24149  prdsxmslem2  24558  curry2ima  32724  fnchoice  44967  fsneqrn  45154  stoweidlem35  45991