Theorem dffn4 6759

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ran crn 5632   Fn wfn 6494  –onto→wfo 6497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fo 6505

This theorem is referenced by:  funforn  6760  fimadmfo  6762  ffoss  7899  tposf2  8200  rneqdmfinf1o  9243  fidomdm  9244  indexfi  9270  intrnfi  9329  fifo  9345  ixpiunwdom  9505  infpwfien  9984  infmap2  10139  cfflb  10181  cfslb2n  10190  ttukeylem6  10436  dmct  10446  fnrndomg  10458  rankcf  10700  tskuni  10706  tskurn  10712  fseqsupcl  13939  s7f1o  14928  vdwlem6  16957  0ram2  16992  0ramcl  16994  quslem  17507  gsumval3  19882  gsumzoppg  19919  mplsubrglem  21982  rncmp  23361  cmpsub  23365  tgcmp  23366  hauscmplem  23371  conncn  23391  2ndcctbss  23420  2ndcomap  23423  2ndcsep  23424  comppfsc  23497  ptcnplem  23586  txtube  23605  txcmplem1  23606  tx1stc  23615  tx2ndc  23616  qtopid  23670  qtopcmplem  23672  qtopkgen  23675  kqtopon  23692  kqopn  23699  kqcld  23700  qtopf1  23781  rnelfm  23918  fmfnfmlem2  23920  fmfnfm  23923  alexsubALT  24016  ptcmplem2  24018  tmdgsum2  24061  tsmsxplem1  24118  met1stc  24486  met2ndci  24487  uniiccdif  25545  dyadmbl  25567  mbfimaopnlem  25622  i1fadd  25662  i1fmul  25663  i1fmulc  25670  mbfi1fseqlem4  25685  limciun  25861  aannenlem3  26296  efabl  26514  logccv  26627  locfinreflem  33984  mvrsfpw  35688  msrfo  35728  mtyf  35734  bj-inftyexpitaufo  37516  itg2addnclem2  37993  istotbnd3  38092  sstotbnd  38096  prdsbnd  38114  cntotbnd  38117  heiborlem1  38132  heibor  38142  dihintcl  41790  focofob  47522