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

Theorem dffn2 5732
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 3524 . . 3  |-  ran  F  C_ 
_V
21biantru 505 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  C_ 
_V ) )
3 df-f 5592 . 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 3113    C_ wss 3476   ran crn 5000    Fn wfn 5583   -->wf 5584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3115  df-in 3483  df-ss 3490  df-f 5592
This theorem is referenced by:  f1cnvcnv  5789  fcoconst  6058  fnressn  6073  fndifnfp  6090  1stcof  6812  2ndcof  6813  fnmpt2  6852  tposfn  6984  tz7.48lem  7106  seqomlem2  7116  mptelixpg  7506  r111  8193  smobeth  8961  inar1  9153  imasvscafn  14792  fucidcl  15192  fucsect  15199  curfcl  15359  curf2ndf  15374  dsmmbas2  18563  frlmsslsp  18624  frlmsslspOLD  18625  frlmup1  18627  prdstopn  19892  prdstps  19893  ist0-4  19993  ptuncnv  20071  xpstopnlem2  20075  prdstgpd  20386  prdsxmslem2  20795  curry2ima  27226  fnchoice  31010  stoweidlem35  31363
  Copyright terms: Public domain W3C validator