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

Theorem dffn3 5677
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 3486 . . 3  |-  ran  F  C_ 
ran  F
21biantru 505 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  C_ 
ran  F ) )
3 df-f 5533 . 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 3439   ran crn 4952    Fn wfn 5524   -->wf 5525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3446  df-ss 3453  df-f 5533
This theorem is referenced by:  fsn2  5995  fo2ndf  6792  fndmfisuppfi  7746  fndmfifsupp  7747  cantnflem1c  8009  fin23lem17  8621  fin23lem32  8627  yoniso  15217  1stckgen  19262  ovolicc2  21140  itg1val2  21298  i1fadd  21309  i1fmul  21310  itg1addlem4  21313  i1fmulc  21317  ofpreima2  26156  fnct  26184  pl1cn  26550  ghomgrpilem2  27469  itg2addnclem2  28612  stoweidlem29  29992  stoweidlem31  29994  stoweidlem59  30022  frgrancvvdeqlemB  30799  mapdcl  35656
  Copyright terms: Public domain W3C validator