Theorem dffn4 6121

Description: A function maps onto its range. (Contributed by NM, 10-May-1998.)

Assertion

Ref	Expression
dffn4	|- ( F Fn A <-> F : A -onto-> ran F )

Proof of Theorem dffn4

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3 |- ran F = ran F
2	1	biantru 526	. 2 |- ( F Fn A <-> ( F Fn A /\ ran F = ran F ) )
3		df-fo 5894	. 2 |- ( F : A -onto-> ran F <-> ( F Fn A /\ ran F = ran F ) )
4	2, 3	bitr4i 267	1 |- ( F Fn A <-> F : A -onto-> ran F )

Syntax hints:   <-> wb 196   /\ wa 384   = wceq 1483   ran crn 5115   Fn wfn 5883   -onto->wfo 5886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-fo 5894

This theorem is referenced by:  funforn  6122  ffoss  7127  tposf2  7376  mapsn  7899  rneqdmfinf1o  8242  fidomdm  8243  pwfilem  8260  indexfi  8274  intrnfi  8322  fifo  8338  ixpiunwdom  8496  infpwfien  8885  infmap2  9040  cfflb  9081  cfslb2n  9090  ttukeylem6  9336  dmct  9346  fnrndomg  9358  rankcf  9599  tskuni  9605  tskurn  9611  fseqsupcl  12776  vdwlem6  15690  0ram2  15725  0ramcl  15727  quslem  16203  gsumval3  18308  gsumzoppg  18344  mplsubrglem  19439  rncmp  21199  cmpsub  21203  tgcmp  21204  hauscmplem  21209  conncn  21229  2ndcctbss  21258  2ndcomap  21261  2ndcsep  21262  comppfsc  21335  ptcnplem  21424  txtube  21443  txcmplem1  21444  tx1stc  21453  tx2ndc  21454  qtopid  21508  qtopcmplem  21510  qtopkgen  21513  kqtopon  21530  kqopn  21537  kqcld  21538  qtopf1  21619  rnelfm  21757  fmfnfmlem2  21759  fmfnfm  21762  alexsubALT  21855  ptcmplem2  21857  tmdgsum2  21900  tsmsxplem1  21956  met1stc  22326  met2ndci  22327  uniiccdif  23346  dyadmbl  23368  mbfimaopnlem  23422  i1fadd  23462  i1fmul  23463  itg1addlem4  23466  i1fmulc  23470  mbfi1fseqlem4  23485  limciun  23658  aannenlem3  24085  efabl  24296  logccv  24409  locfinreflem  29907  mvrsfpw  31403  msrfo  31443  mtyf  31449  itg2addnclem2  33462  istotbnd3  33570  sstotbnd  33574  prdsbnd  33592  cntotbnd  33595  heiborlem1  33610  heibor  33620  dihintcl  36633  mapsnd  39388