Theorem dffn4 6814

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

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1533  ran crn 5678   Fn wfn 6542  –onto→wfo 6545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-fo 6553

This theorem is referenced by:  funforn  6815  fimadmfo  6817  ffoss  7948  tposf2  8254  rneqdmfinf1o  9352  fidomdm  9353  pwfilemOLD  9370  indexfi  9384  intrnfi  9439  fifo  9455  ixpiunwdom  9613  infpwfien  10085  infmap2  10241  cfflb  10282  cfslb2n  10291  ttukeylem6  10537  dmct  10547  fnrndomg  10559  rankcf  10800  tskuni  10806  tskurn  10812  fseqsupcl  13974  vdwlem6  16954  0ram2  16989  0ramcl  16991  quslem  17524  gsumval3  19866  gsumzoppg  19903  mplsubrglem  21953  rncmp  23330  cmpsub  23334  tgcmp  23335  hauscmplem  23340  conncn  23360  2ndcctbss  23389  2ndcomap  23392  2ndcsep  23393  comppfsc  23466  ptcnplem  23555  txtube  23574  txcmplem1  23575  tx1stc  23584  tx2ndc  23585  qtopid  23639  qtopcmplem  23641  qtopkgen  23644  kqtopon  23661  kqopn  23668  kqcld  23669  qtopf1  23750  rnelfm  23887  fmfnfmlem2  23889  fmfnfm  23892  alexsubALT  23985  ptcmplem2  23987  tmdgsum2  24030  tsmsxplem1  24087  met1stc  24460  met2ndci  24461  uniiccdif  25537  dyadmbl  25559  mbfimaopnlem  25614  i1fadd  25654  i1fmul  25655  itg1addlem4OLD  25659  i1fmulc  25663  mbfi1fseqlem4  25678  limciun  25853  aannenlem3  26295  efabl  26514  logccv  26627  locfinreflem  33511  mvrsfpw  35186  msrfo  35226  mtyf  35232  bj-inftyexpitaufo  36751  itg2addnclem2  37215  istotbnd3  37314  sstotbnd  37318  prdsbnd  37336  cntotbnd  37339  heiborlem1  37354  heibor  37364  dihintcl  40886  focofob  46523