Theorem dffn4 6737

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 2730	. . 3 ⊢ ran 𝐹 = ran 𝐹
2	1	biantru 529	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3		df-fo 6483	. 2 ⊢ (𝐹:𝐴–onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
4	2, 3	bitr4i 278	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  ran crn 5615   Fn wfn 6472  –onto→wfo 6475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2722  df-fo 6483

This theorem is referenced by:  funforn  6738  fimadmfo  6740  ffoss  7873  tposf2  8175  rneqdmfinf1o  9212  fidomdm  9213  indexfi  9239  intrnfi  9295  fifo  9311  ixpiunwdom  9471  infpwfien  9945  infmap2  10100  cfflb  10142  cfslb2n  10151  ttukeylem6  10397  dmct  10407  fnrndomg  10419  rankcf  10660  tskuni  10666  tskurn  10672  fseqsupcl  13876  s7f1o  14865  vdwlem6  16890  0ram2  16925  0ramcl  16927  quslem  17439  gsumval3  19812  gsumzoppg  19849  mplsubrglem  21934  rncmp  23304  cmpsub  23308  tgcmp  23309  hauscmplem  23314  conncn  23334  2ndcctbss  23363  2ndcomap  23366  2ndcsep  23367  comppfsc  23440  ptcnplem  23529  txtube  23548  txcmplem1  23549  tx1stc  23558  tx2ndc  23559  qtopid  23613  qtopcmplem  23615  qtopkgen  23618  kqtopon  23635  kqopn  23642  kqcld  23643  qtopf1  23724  rnelfm  23861  fmfnfmlem2  23863  fmfnfm  23866  alexsubALT  23959  ptcmplem2  23961  tmdgsum2  24004  tsmsxplem1  24061  met1stc  24429  met2ndci  24430  uniiccdif  25499  dyadmbl  25521  mbfimaopnlem  25576  i1fadd  25616  i1fmul  25617  i1fmulc  25624  mbfi1fseqlem4  25639  limciun  25815  aannenlem3  26258  efabl  26479  logccv  26592  locfinreflem  33843  mvrsfpw  35518  msrfo  35558  mtyf  35564  bj-inftyexpitaufo  37215  itg2addnclem2  37691  istotbnd3  37790  sstotbnd  37794  prdsbnd  37812  cntotbnd  37815  heiborlem1  37830  heibor  37840  dihintcl  41362  focofob  47090