Theorem dffn2 6749

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

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3488   ⊆ wss 3976  ran crn 5701   Fn wfn 6568  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-f 6577

This theorem is referenced by:  f1cnvcnv  6826  fcoconst  7168  fnressn  7192  fndifnfp  7210  1stcof  8060  2ndcof  8061  fnmpo  8110  tposfn  8296  tz7.48lem  8497  seqomlem2  8507  mptelixpg  8993  r111  9844  smobeth  10655  inar1  10844  imasvscafn  17597  fucidcl  18035  fucsect  18042  dfinito3  18072  dftermo3  18073  curfcl  18302  curf2ndf  18317  dsmmbas2  21780  frlmsslsp  21839  frlmup1  21841  prdstopn  23657  prdstps  23658  ist0-4  23758  ptuncnv  23836  xpstopnlem2  23840  prdstgpd  24154  prdsxmslem2  24563  curry2ima  32720  fnchoice  44929  fsneqrn  45118  stoweidlem35  45956