Theorem dffn4 6840

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537  ran crn 5701   Fn wfn 6568  –onto→wfo 6571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-fo 6579

This theorem is referenced by:  funforn  6841  fimadmfo  6843  ffoss  7986  tposf2  8291  rneqdmfinf1o  9401  fidomdm  9402  pwfilemOLD  9416  indexfi  9430  intrnfi  9485  fifo  9501  ixpiunwdom  9659  infpwfien  10131  infmap2  10286  cfflb  10328  cfslb2n  10337  ttukeylem6  10583  dmct  10593  fnrndomg  10605  rankcf  10846  tskuni  10852  tskurn  10858  fseqsupcl  14028  s7f1o  15015  vdwlem6  17033  0ram2  17068  0ramcl  17070  quslem  17603  gsumval3  19949  gsumzoppg  19986  mplsubrglem  22047  rncmp  23425  cmpsub  23429  tgcmp  23430  hauscmplem  23435  conncn  23455  2ndcctbss  23484  2ndcomap  23487  2ndcsep  23488  comppfsc  23561  ptcnplem  23650  txtube  23669  txcmplem1  23670  tx1stc  23679  tx2ndc  23680  qtopid  23734  qtopcmplem  23736  qtopkgen  23739  kqtopon  23756  kqopn  23763  kqcld  23764  qtopf1  23845  rnelfm  23982  fmfnfmlem2  23984  fmfnfm  23987  alexsubALT  24080  ptcmplem2  24082  tmdgsum2  24125  tsmsxplem1  24182  met1stc  24555  met2ndci  24556  uniiccdif  25632  dyadmbl  25654  mbfimaopnlem  25709  i1fadd  25749  i1fmul  25750  itg1addlem4OLD  25754  i1fmulc  25758  mbfi1fseqlem4  25773  limciun  25949  aannenlem3  26390  efabl  26610  logccv  26723  locfinreflem  33786  mvrsfpw  35474  msrfo  35514  mtyf  35520  bj-inftyexpitaufo  37168  itg2addnclem2  37632  istotbnd3  37731  sstotbnd  37735  prdsbnd  37753  cntotbnd  37756  heiborlem1  37771  heibor  37781  dihintcl  41301  focofob  46995