Theorem dffn4 6812

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

Assertion

Ref	Expression
dffn4	⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)

Proof of Theorem dffn4

Step	Hyp	Ref	Expression
1		eqid 2733	. . 3 ⊢ ran 𝐹 = ran 𝐹
2	1	biantru 531	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3		df-fo 6550	. 2 ⊢ (𝐹:𝐴–onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
4	2, 3	bitr4i 278	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)

Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1542  ran crn 5678   Fn wfn 6539  –onto→wfo 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fo 6550

This theorem is referenced by:  funforn  6813  fimadmfo  6815  ffoss  7932  tposf2  8235  rneqdmfinf1o  9328  fidomdm  9329  pwfilemOLD  9346  indexfi  9360  intrnfi  9411  fifo  9427  ixpiunwdom  9585  infpwfien  10057  infmap2  10213  cfflb  10254  cfslb2n  10263  ttukeylem6  10509  dmct  10519  fnrndomg  10531  rankcf  10772  tskuni  10778  tskurn  10784  fseqsupcl  13942  vdwlem6  16919  0ram2  16954  0ramcl  16956  quslem  17489  gsumval3  19775  gsumzoppg  19812  mplsubrglem  21563  rncmp  22900  cmpsub  22904  tgcmp  22905  hauscmplem  22910  conncn  22930  2ndcctbss  22959  2ndcomap  22962  2ndcsep  22963  comppfsc  23036  ptcnplem  23125  txtube  23144  txcmplem1  23145  tx1stc  23154  tx2ndc  23155  qtopid  23209  qtopcmplem  23211  qtopkgen  23214  kqtopon  23231  kqopn  23238  kqcld  23239  qtopf1  23320  rnelfm  23457  fmfnfmlem2  23459  fmfnfm  23462  alexsubALT  23555  ptcmplem2  23557  tmdgsum2  23600  tsmsxplem1  23657  met1stc  24030  met2ndci  24031  uniiccdif  25095  dyadmbl  25117  mbfimaopnlem  25172  i1fadd  25212  i1fmul  25213  itg1addlem4OLD  25217  i1fmulc  25221  mbfi1fseqlem4  25236  limciun  25411  aannenlem3  25843  efabl  26059  logccv  26171  locfinreflem  32820  mvrsfpw  34497  msrfo  34537  mtyf  34543  bj-inftyexpitaufo  36083  itg2addnclem2  36540  istotbnd3  36639  sstotbnd  36643  prdsbnd  36661  cntotbnd  36664  heiborlem1  36679  heibor  36689  dihintcl  40215  focofob  45788