Theorem dffn4 6692

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

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1542  ran crn 5591   Fn wfn 6427  –onto→wfo 6430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-cleq 2732  df-fo 6438

This theorem is referenced by:  funforn  6693  fimadmfo  6695  ffoss  7782  tposf2  8057  rneqdmfinf1o  9073  fidomdm  9074  pwfilemOLD  9091  indexfi  9105  intrnfi  9153  fifo  9169  ixpiunwdom  9327  infpwfien  9819  infmap2  9975  cfflb  10016  cfslb2n  10025  ttukeylem6  10271  dmct  10281  fnrndomg  10293  rankcf  10534  tskuni  10540  tskurn  10546  fseqsupcl  13695  vdwlem6  16685  0ram2  16720  0ramcl  16722  quslem  17252  gsumval3  19506  gsumzoppg  19543  mplsubrglem  21208  rncmp  22545  cmpsub  22549  tgcmp  22550  hauscmplem  22555  conncn  22575  2ndcctbss  22604  2ndcomap  22607  2ndcsep  22608  comppfsc  22681  ptcnplem  22770  txtube  22789  txcmplem1  22790  tx1stc  22799  tx2ndc  22800  qtopid  22854  qtopcmplem  22856  qtopkgen  22859  kqtopon  22876  kqopn  22883  kqcld  22884  qtopf1  22965  rnelfm  23102  fmfnfmlem2  23104  fmfnfm  23107  alexsubALT  23200  ptcmplem2  23202  tmdgsum2  23245  tsmsxplem1  23302  met1stc  23675  met2ndci  23676  uniiccdif  24740  dyadmbl  24762  mbfimaopnlem  24817  i1fadd  24857  i1fmul  24858  itg1addlem4OLD  24862  i1fmulc  24866  mbfi1fseqlem4  24881  limciun  25056  aannenlem3  25488  efabl  25704  logccv  25816  locfinreflem  31786  mvrsfpw  33464  msrfo  33504  mtyf  33510  bj-inftyexpitaufo  35369  itg2addnclem2  35825  istotbnd3  35925  sstotbnd  35929  prdsbnd  35947  cntotbnd  35950  heiborlem1  35965  heibor  35975  dihintcl  39354  focofob  44540