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

Theorem dffn2 5640
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 3437 . . 3  |-  ran  F  C_ 
_V
21biantru 503 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  C_ 
_V ) )
3 df-f 5500 . 2  |-  ( F : A --> _V  <->  ( F  Fn  A  /\  ran  F  C_ 
_V ) )
42, 3bitr4i 252 1  |-  ( F  Fn  A  <->  F : A
--> _V )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367   _Vcvv 3034    C_ wss 3389   ran crn 4914    Fn wfn 5491   -->wf 5492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-v 3036  df-in 3396  df-ss 3403  df-f 5500
This theorem is referenced by:  f1cnvcnv  5697  fcoconst  5970  fnressn  5985  fndifnfp  6002  1stcof  6727  2ndcof  6728  fnmpt2  6767  tposfn  6902  tz7.48lem  7024  seqomlem2  7034  mptelixpg  7425  r111  8106  smobeth  8874  inar1  9064  imasvscafn  14944  fucidcl  15371  fucsect  15378  curfcl  15618  curf2ndf  15633  dsmmbas2  18859  frlmsslsp  18916  frlmup1  18918  prdstopn  20214  prdstps  20215  ist0-4  20315  ptuncnv  20393  xpstopnlem2  20397  prdstgpd  20708  prdsxmslem2  21117  curry2ima  27674  fnchoice  31571  stoweidlem35  31983
  Copyright terms: Public domain W3C validator