Theorem dffn2 6602

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 3945	. . 3 ⊢ ran 𝐹 ⊆ V
2	1	biantru 530	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 6437	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 277	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 205   ∧ wa 396  Vcvv 3432   ⊆ wss 3887  ran crn 5590   Fn wfn 6428  ⟶wf 6429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-f 6437

This theorem is referenced by:  f1cnvcnv  6680  fcoconst  7006  fnressn  7030  fndifnfp  7048  1stcof  7861  2ndcof  7862  fnmpo  7909  tposfn  8071  tz7.48lem  8272  seqomlem2  8282  mptelixpg  8723  r111  9533  smobeth  10342  inar1  10531  imasvscafn  17248  fucidcl  17683  fucsect  17690  dfinito3  17720  dftermo3  17721  curfcl  17950  curf2ndf  17965  dsmmbas2  20944  frlmsslsp  21003  frlmup1  21005  prdstopn  22779  prdstps  22780  ist0-4  22880  ptuncnv  22958  xpstopnlem2  22962  prdstgpd  23276  prdsxmslem2  23685  curry2ima  31041  fnchoice  42572  fsneqrn  42751  stoweidlem35  43576