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

Proof of Theorem dffn3
StepHypRef Expression
1 ssid 3528 . . 3
21biantru 505 . 2
3 df-f 5598 . 2
42, 3bitr4i 252 1
 Colors of variables: wff setvar class Syntax hints:   wb 184   wa 369   wss 3481   crn 5006   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