Theorem dffn2 5960

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

Syntax hints:   ↔ wb 195   ∧ wa 383  Vcvv 3173   ⊆ wss 3540  ran crn 5039   Fn wfn 5799  ⟶wf 5800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175  df-in 3547  df-ss 3554  df-f 5808

This theorem is referenced by:  f1cnvcnv  6022  fcoconst  6307  fnressn  6330  fndifnfp  6347  1stcof  7087  2ndcof  7088  fnmpt2  7127  tposfn  7268  tz7.48lem  7423  seqomlem2  7433  mptelixpg  7831  r111  8521  smobeth  9287  inar1  9476  imasvscafn  16020  fucidcl  16448  fucsect  16455  curfcl  16695  curf2ndf  16710  dsmmbas2  19900  frlmsslsp  19954  frlmup1  19956  prdstopn  21241  prdstps  21242  ist0-4  21342  ptuncnv  21420  xpstopnlem2  21424  prdstgpd  21738  prdsxmslem2  22144  curry2ima  28869  fnchoice  38211  fsneqrn  38398  stoweidlem35  38928