MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dffn2 Structured version   Unicode version

Theorem dffn2 5690
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  |-  ( F  Fn  A  <->  F : A
--> _V )

Proof of Theorem dffn2
StepHypRef Expression
1 ssv 3427 . . 3  |-  ran  F  C_ 
_V
21biantru 507 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  C_ 
_V ) )
3 df-f 5548 . 2  |-  ( F : A --> _V  <->  ( F  Fn  A  /\  ran  F  C_ 
_V ) )
42, 3bitr4i 255 1  |-  ( F  Fn  A  <->  F : A
--> _V )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370   _Vcvv 3022    C_ wss 3379   ran crn 4797    Fn wfn 5539   -->wf 5540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-v 3024  df-in 3386  df-ss 3393  df-f 5548
This theorem is referenced by:  f1cnvcnv  5747  fcoconst  6019  fnressn  6035  fndifnfp  6052  1stcof  6779  2ndcof  6780  fnmpt2  6819  tposfn  6957  tz7.48lem  7113  seqomlem2  7123  mptelixpg  7514  r111  8198  smobeth  8962  inar1  9151  imasvscafn  15386  fucidcl  15813  fucsect  15820  curfcl  16060  curf2ndf  16075  dsmmbas2  19242  frlmsslsp  19296  frlmup1  19298  prdstopn  20585  prdstps  20586  ist0-4  20686  ptuncnv  20764  xpstopnlem2  20768  prdstgpd  21081  prdsxmslem2  21486  curry2ima  28235  fnchoice  37266  stoweidlem35  37779
  Copyright terms: Public domain W3C validator