Theorem dffn3 5743

Description: A function maps to its range. (Contributed by NM, 1-Sep-1999.)

Assertion

Ref	Expression
dffn3

Proof of Theorem dffn3

Step	Hyp	Ref	Expression
1		ssid 3522	. . 3
2	1	biantru 505	. 2
3		df-f 5597	. 2
4	2, 3	bitr4i 252	1

Syntax hints:  <->wb 184  /\wa 369  C_wss 3475  rancrn 5005  Fnwfn 5588  -->wf 5589

This theorem is referenced by:  fsn2  6071  fo2ndf  6907  fndmfisuppfi  7861  fndmfifsupp  7862  fin23lem17  8739  fin23lem32  8745  yoniso  15554  1stckgen  20055  ovolicc2  21933  itg1val2  22091  i1fadd  22102  i1fmul  22103  itg1addlem4  22106  i1fmulc  22110  frgrancvvdeqlemB  25038  foresf1o  27403  fcoinver  27460  ofpreima2  27508  fnct  27536  locfinreflem  27843  pl1cn  27937  ghomgrpilem2  29026  itg2addnclem2  30067  icccncfext  31690  stoweidlem29  31811  stoweidlem31  31813  stoweidlem59  31841  mapdcl  37380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-f 5597