Theorem dffn4 6690

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

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1541  ran crn 5589   Fn wfn 6425  –onto→wfo 6428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731  df-fo 6436

This theorem is referenced by:  funforn  6691  fimadmfo  6693  ffoss  7775  tposf2  8050  rneqdmfinf1o  9056  fidomdm  9057  pwfilemOLD  9074  indexfi  9088  intrnfi  9136  fifo  9152  ixpiunwdom  9310  infpwfien  9802  infmap2  9958  cfflb  9999  cfslb2n  10008  ttukeylem6  10254  dmct  10264  fnrndomg  10276  rankcf  10517  tskuni  10523  tskurn  10529  fseqsupcl  13678  vdwlem6  16668  0ram2  16703  0ramcl  16705  quslem  17235  gsumval3  19489  gsumzoppg  19526  mplsubrglem  21191  rncmp  22528  cmpsub  22532  tgcmp  22533  hauscmplem  22538  conncn  22558  2ndcctbss  22587  2ndcomap  22590  2ndcsep  22591  comppfsc  22664  ptcnplem  22753  txtube  22772  txcmplem1  22773  tx1stc  22782  tx2ndc  22783  qtopid  22837  qtopcmplem  22839  qtopkgen  22842  kqtopon  22859  kqopn  22866  kqcld  22867  qtopf1  22948  rnelfm  23085  fmfnfmlem2  23087  fmfnfm  23090  alexsubALT  23183  ptcmplem2  23185  tmdgsum2  23228  tsmsxplem1  23285  met1stc  23658  met2ndci  23659  uniiccdif  24723  dyadmbl  24745  mbfimaopnlem  24800  i1fadd  24840  i1fmul  24841  itg1addlem4OLD  24845  i1fmulc  24849  mbfi1fseqlem4  24864  limciun  25039  aannenlem3  25471  efabl  25687  logccv  25799  locfinreflem  31769  mvrsfpw  33447  msrfo  33487  mtyf  33493  bj-inftyexpitaufo  35352  itg2addnclem2  35808  istotbnd3  35908  sstotbnd  35912  prdsbnd  35930  cntotbnd  35933  heiborlem1  35948  heibor  35958  dihintcl  39337  focofob  44523