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

Theorem dffn3 5720
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 3508 . . 3  |-  ran  F  C_ 
ran  F
21biantru 503 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  C_ 
ran  F ) )
3 df-f 5574 . 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 367    C_ wss 3461   ran crn 4989    Fn wfn 5565   -->wf 5566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475  df-f 5574
This theorem is referenced by:  fsn2  6047  fo2ndf  6880  fndmfisuppfi  7833  fndmfifsupp  7834  fin23lem17  8709  fin23lem32  8715  yoniso  15756  1stckgen  20224  ovolicc2  22102  itg1val2  22260  i1fadd  22271  i1fmul  22272  itg1addlem4  22275  i1fmulc  22279  frgrancvvdeqlemB  25243  foresf1o  27605  fcoinver  27677  ofpreima2  27738  fnct  27769  locfinreflem  28081  pl1cn  28175  ghomgrpilem2  29293  itg2addnclem2  30310  icccncfext  31932  stoweidlem29  32053  stoweidlem31  32055  stoweidlem59  32083  mapdcl  37796
  Copyright terms: Public domain W3C validator