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

Theorem dffn2 5390
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 3198 . . 3  |-  ran  F  C_ 
_V
21biantru 491 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  C_ 
_V ) )
3 df-f 5259 . 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 2788    C_ wss 3152   ran crn 4690    Fn wfn 5250   -->wf 5251
This theorem is referenced by:  f1cnvcnv  5445  fcoconst  5695  fnressn  5705  1stcof  6147  2ndcof  6148  fnmpt2  6192  tposfn  6263  tz7.48lem  6453  seqomlem2  6463  mptelixpg  6853  r111  7447  smobeth  8208  inar1  8397  imasvscafn  13439  fucidcl  13839  fucsect  13846  curfcl  14006  curf2ndf  14021  prdstopn  17322  prdstps  17323  ist0-4  17420  ptuncnv  17498  xpstopnlem2  17502  prdstgpd  17807  prdsxmslem2  18075  curry2ima  23247  cbicp  25166  fndifnfp  26756  dsmmbas2  27203  frlmsslsp  27248  frlmup1  27250  fnchoice  27700  stoweidlem35  27784
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790  df-in 3159  df-ss 3166  df-f 5259
  Copyright terms: Public domain W3C validator