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

Theorem dffn3 5476
Description: A function maps to its range. (Contributed by NM, 1-Sep-1999.)
Assertion
Ref Expression
dffn3  |-  ( F  Fn  A  <->  F : A
--> ran  F )

Proof of Theorem dffn3
StepHypRef Expression
1 ssid 3273 . . 3  |-  ran  F  C_ 
ran  F
21biantru 491 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  C_ 
ran  F ) )
3 df-f 5338 . 2  |-  ( F : A --> ran  F  <->  ( F  Fn  A  /\  ran  F  C_  ran  F ) )
42, 3bitr4i 243 1  |-  ( F  Fn  A  <->  F : A
--> ran  F )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    C_ wss 3228   ran crn 4769    Fn wfn 5329   -->wf 5330
This theorem is referenced by:  fsn2  5778  fin23lem17  8051  fin23lem32  8057  yoniso  14152  1stckgen  17349  ovolicc2  18979  itg1val2  19137  i1fadd  19148  i1fmul  19149  itg1addlem4  19152  i1fmulc  19156  fnct  23306  ghomgrpilem2  24397  itg2addnclem2  25493  stoweidlem29  27101  stoweidlem31  27103  stoweidlem59  27131  frgrancvvdeqlemB  27854  mapdcl  31895
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-in 3235  df-ss 3242  df-f 5338
  Copyright terms: Public domain W3C validator