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

Theorem dffn2 5559
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 3375 . . 3  |-  ran  F  C_ 
_V
21biantru 505 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  C_ 
_V ) )
3 df-f 5421 . 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 369   _Vcvv 2971    C_ wss 3327   ran crn 4840    Fn wfn 5412   -->wf 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-v 2973  df-in 3334  df-ss 3341  df-f 5421
This theorem is referenced by:  f1cnvcnv  5613  fcoconst  5879  fnressn  5893  fndifnfp  5906  1stcof  6603  2ndcof  6604  fnmpt2  6641  tposfn  6773  tz7.48lem  6895  seqomlem2  6905  mptelixpg  7299  r111  7981  smobeth  8749  inar1  8941  imasvscafn  14474  fucidcl  14874  fucsect  14881  curfcl  15041  curf2ndf  15056  dsmmbas2  18161  frlmsslsp  18222  frlmsslspOLD  18223  frlmup1  18225  prdstopn  19200  prdstps  19201  ist0-4  19301  ptuncnv  19379  xpstopnlem2  19383  prdstgpd  19694  prdsxmslem2  20103  curry2ima  26002  fnchoice  29749  stoweidlem35  29828
  Copyright terms: Public domain W3C validator