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

Theorem dffn3 5744
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 3528 . . 3  |-  ran  F  C_ 
ran  F
21biantru 505 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  C_ 
ran  F ) )
3 df-f 5598 . 2  |-  ( F : A --> ran  F  <->  ( F  Fn  A  /\  ran  F  C_  ran  F ) )
42, 3bitr4i 252 1  |-  ( F  Fn  A  <->  F : A
--> ran  F )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    C_ wss 3481   ran crn 5006    Fn wfn 5589   -->wf 5590
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-in 3488  df-ss 3495  df-f 5598
This theorem is referenced by:  fsn2  6072  fo2ndf  6902  fndmfisuppfi  7853  fndmfifsupp  7854  cantnflem1c  8118  fin23lem17  8730  fin23lem32  8736  yoniso  15429  1stckgen  19923  ovolicc2  21801  itg1val2  21959  i1fadd  21970  i1fmul  21971  itg1addlem4  21974  i1fmulc  21978  frgrancvvdeqlemB  24862  foresf1o  27226  fcoinver  27283  ofpreima2  27331  fnct  27359  locfinreflem  27668  pl1cn  27762  ghomgrpilem2  28851  itg2addnclem2  29994  icccncfext  31549  stoweidlem29  31652  stoweidlem31  31654  stoweidlem59  31682  mapdcl  36851
  Copyright terms: Public domain W3C validator