Theorem dffn4 6724

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

Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1539  ran crn 5601   Fn wfn 6453  –onto→wfo 6456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728  df-fo 6464

This theorem is referenced by:  funforn  6725  fimadmfo  6727  ffoss  7820  tposf2  8097  rneqdmfinf1o  9143  fidomdm  9144  pwfilemOLD  9161  indexfi  9175  intrnfi  9223  fifo  9239  ixpiunwdom  9397  infpwfien  9868  infmap2  10024  cfflb  10065  cfslb2n  10074  ttukeylem6  10320  dmct  10330  fnrndomg  10342  rankcf  10583  tskuni  10589  tskurn  10595  fseqsupcl  13747  vdwlem6  16736  0ram2  16771  0ramcl  16773  quslem  17303  gsumval3  19557  gsumzoppg  19594  mplsubrglem  21259  rncmp  22596  cmpsub  22600  tgcmp  22601  hauscmplem  22606  conncn  22626  2ndcctbss  22655  2ndcomap  22658  2ndcsep  22659  comppfsc  22732  ptcnplem  22821  txtube  22840  txcmplem1  22841  tx1stc  22850  tx2ndc  22851  qtopid  22905  qtopcmplem  22907  qtopkgen  22910  kqtopon  22927  kqopn  22934  kqcld  22935  qtopf1  23016  rnelfm  23153  fmfnfmlem2  23155  fmfnfm  23158  alexsubALT  23251  ptcmplem2  23253  tmdgsum2  23296  tsmsxplem1  23353  met1stc  23726  met2ndci  23727  uniiccdif  24791  dyadmbl  24813  mbfimaopnlem  24868  i1fadd  24908  i1fmul  24909  itg1addlem4OLD  24913  i1fmulc  24917  mbfi1fseqlem4  24932  limciun  25107  aannenlem3  25539  efabl  25755  logccv  25867  locfinreflem  31839  mvrsfpw  33517  msrfo  33557  mtyf  33563  bj-inftyexpitaufo  35421  itg2addnclem2  35877  istotbnd3  35977  sstotbnd  35981  prdsbnd  35999  cntotbnd  36002  heiborlem1  36017  heibor  36027  dihintcl  39558  focofob  44816