Theorem dffn2 6085

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 3658	. . 3 ⊢ ran 𝐹 ⊆ V
2	1	biantru 525	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 5930	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 267	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 196   ∧ wa 383  Vcvv 3231   ⊆ wss 3607  ran crn 5144   Fn wfn 5921  ⟶wf 5922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233  df-in 3614  df-ss 3621  df-f 5930

This theorem is referenced by:  f1cnvcnv  6147  fcoconst  6441  fnressn  6465  fndifnfp  6483  1stcof  7240  2ndcof  7241  fnmpt2  7283  tposfn  7426  tz7.48lem  7581  seqomlem2  7591  mptelixpg  7987  r111  8676  smobeth  9446  inar1  9635  imasvscafn  16244  fucidcl  16672  fucsect  16679  curfcl  16919  curf2ndf  16934  dsmmbas2  20129  frlmsslsp  20183  frlmup1  20185  prdstopn  21479  prdstps  21480  ist0-4  21580  ptuncnv  21658  xpstopnlem2  21662  prdstgpd  21975  prdsxmslem2  22381  curry2ima  29614  fnchoice  39502  fsneqrn  39717  stoweidlem35  40570