Theorem dffn4 6811

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

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1534  ran crn 5673   Fn wfn 6537  –onto→wfo 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2719  df-fo 6548

This theorem is referenced by:  funforn  6812  fimadmfo  6814  ffoss  7943  tposf2  8249  rneqdmfinf1o  9344  fidomdm  9345  pwfilemOLD  9362  indexfi  9376  intrnfi  9431  fifo  9447  ixpiunwdom  9605  infpwfien  10077  infmap2  10233  cfflb  10274  cfslb2n  10283  ttukeylem6  10529  dmct  10539  fnrndomg  10551  rankcf  10792  tskuni  10798  tskurn  10804  fseqsupcl  13966  vdwlem6  16946  0ram2  16981  0ramcl  16983  quslem  17516  gsumval3  19853  gsumzoppg  19890  mplsubrglem  21933  rncmp  23287  cmpsub  23291  tgcmp  23292  hauscmplem  23297  conncn  23317  2ndcctbss  23346  2ndcomap  23349  2ndcsep  23350  comppfsc  23423  ptcnplem  23512  txtube  23531  txcmplem1  23532  tx1stc  23541  tx2ndc  23542  qtopid  23596  qtopcmplem  23598  qtopkgen  23601  kqtopon  23618  kqopn  23625  kqcld  23626  qtopf1  23707  rnelfm  23844  fmfnfmlem2  23846  fmfnfm  23849  alexsubALT  23942  ptcmplem2  23944  tmdgsum2  23987  tsmsxplem1  24044  met1stc  24417  met2ndci  24418  uniiccdif  25494  dyadmbl  25516  mbfimaopnlem  25571  i1fadd  25611  i1fmul  25612  itg1addlem4OLD  25616  i1fmulc  25620  mbfi1fseqlem4  25635  limciun  25810  aannenlem3  26252  efabl  26471  logccv  26584  locfinreflem  33377  mvrsfpw  35052  msrfo  35092  mtyf  35098  bj-inftyexpitaufo  36617  itg2addnclem2  37080  istotbnd3  37179  sstotbnd  37183  prdsbnd  37201  cntotbnd  37204  heiborlem1  37219  heibor  37229  dihintcl  40754  focofob  46383