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

Theorem dffn2 5406
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 3211 . . 3  |-  ran  F  C_ 
_V
21biantru 491 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  C_ 
_V ) )
3 df-f 5275 . 2  |-  ( F : A --> _V  <->  ( F  Fn  A  /\  ran  F  C_ 
_V ) )
42, 3bitr4i 243 1  |-  ( F  Fn  A  <->  F : A
--> _V )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   _Vcvv 2801    C_ wss 3165   ran crn 4706    Fn wfn 5266   -->wf 5267
This theorem is referenced by:  f1cnvcnv  5461  fcoconst  5711  fnressn  5721  1stcof  6163  2ndcof  6164  fnmpt2  6208  tposfn  6279  tz7.48lem  6469  seqomlem2  6479  mptelixpg  6869  r111  7463  smobeth  8224  inar1  8413  imasvscafn  13455  fucidcl  13855  fucsect  13862  curfcl  14022  curf2ndf  14037  prdstopn  17338  prdstps  17339  ist0-4  17436  ptuncnv  17514  xpstopnlem2  17518  prdstgpd  17823  prdsxmslem2  18091  curry2ima  23262  cbicp  25269  fndifnfp  26859  dsmmbas2  27306  frlmsslsp  27351  frlmup1  27353  fnchoice  27803  stoweidlem35  27887
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-v 2803  df-in 3172  df-ss 3179  df-f 5275
  Copyright terms: Public domain W3C validator