Theorem dffn4 6784

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

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1561  ran crn 5649   Fn wfn 6516  –onto→wfo 6519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-cleq 2755  df-fo 6527

This theorem is referenced by:  funforn  6785  fimadmfo  6787  ffoss  7927  tposf2  8230  rneqdmfinf1o  9274  fidomdm  9275  indexfi  9301  intrnfi  9360  fifo  9376  ixpiunwdom  9536  infpwfien  10030  infmap2  10184  cfflb  10227  cfslb2n  10236  ttukeylem6  10482  dmct  10492  fnrndomg  10504  rankcf  10746  tskuni  10752  tskurn  10758  fseqsupcl  14000  s7f1o  14989  vdwlem6  17032  0ram2  17067  0ramcl  17069  quslem  17583  gsumval3  19957  gsumzoppg  19994  mplsubrglem  22062  rncmp  23463  cmpsub  23467  tgcmp  23468  hauscmplem  23473  conncn  23493  2ndcctbss  23522  2ndcomap  23525  2ndcsep  23526  comppfsc  23599  ptcnplem  23688  txtube  23707  txcmplem1  23708  tx1stc  23717  tx2ndc  23718  qtopid  23772  qtopcmplem  23774  qtopkgen  23777  kqtopon  23794  kqopn  23801  kqcld  23802  qtopf1  23883  rnelfm  24020  fmfnfmlem2  24022  fmfnfm  24025  alexsubALT  24118  ptcmplem2  24120  tmdgsum2  24163  tsmsxplem1  24220  met1stc  24588  met2ndci  24589  uniiccdif  25647  dyadmbl  25669  mbfimaopnlem  25724  i1fadd  25764  i1fmul  25765  i1fmulc  25772  mbfi1fseqlem4  25787  limciun  25963  aannenlem3  26401  efabl  26622  logccv  26735  locfinreflem  34139  mvrsfpw  35861  msrfo  35901  mtyf  35907  bj-inftyexpitaufo  37699  itg2addnclem2  38176  istotbnd3  38275  sstotbnd  38279  prdsbnd  38297  cntotbnd  38300  heiborlem1  38315  heibor  38325  dihintcl  41973  focofob  47665