Theorem dffn4 6824

Description: A function maps onto its range. (Contributed by NM, 10-May-1998.)

Assertion

Ref	Expression
dffn4	⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ontoran 𝐹)

Proof of Theorem dffn4

Step	Hyp	Ref	Expression
1		eqid 2763	. . 3 ⊢ ran 𝐹 = ran 𝐹
2	1	biantru 539	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3		df-fo 6564	. 2 ⊢ (𝐹:𝐴⟶ontoran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
4	2, 3	bitr4i 281	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ontoran 𝐹)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ran crn 5656   Fn wfn 6553  ⟶ontowfo 6556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-fo 6564

This theorem is used by:  funforn  6825  fimadmfo  6827  ffoss  7982  tposf2  8295  rneqdmfinf1o  9350  fidomdm  9351  indexfi  9377  intrnfi  9435  fifo  9451  ixpiunwdom  9611  infpwfien  10168  infmap2  10322  cfflb  10364  cfslb2n  10373  ttukeylem6  10619  dmct  10629  dmctOLD  10630  imadomnum  10641  fnrndomnum  10644  fnrndomgOLD  10646  rankcf  10889  tskuni  10895  tskurn  10901  fseqsupcl  14147  s7f1o  15148  vdwlem6  17193  0ram2  17228  0ramcl  17230  quslem  17744  gsumval3  20151  gsumzoppg  20188  mplsubrglem  22341  rncmp  23744  cmpsub  23748  tgcmp  23749  hauscmplem  23754  conncn  23774  2ndcctbss  23804  2ndcomap  23807  2ndcsep  23808  comppfsc  23881  ptcnplem  23970  txtube  23989  txcmplem1  23990  tx1stc  23999  tx2ndc  24000  qtopid  24054  qtopcmplem  24056  qtopkgen  24059  kqtopon  24076  kqopn  24083  kqcld  24084  qtopf1  24165  rnelfm  24302  fmfnfmlem2  24304  fmfnfm  24307  alexsubALT  24400  ptcmplem2  24402  tmdgsum2  24445  tsmsxplem1  24502  met1stc  24870  met2ndci  24871  uniiccdif  25929  dyadmbl  25951  mbfimaopnlem  26006  i1fadd  26046  i1fmul  26047  i1fmulc  26054  mbfi1fseqlem4  26069  limciun  26244  aannenlem3  26687  efabl  26908  logccv  27021  locfinreflem  34542  mvrsfpw  36438  msrfo  36478  mtyf  36484  bj-inftyexpitaufo  38315  itg2addnclem2  38782  istotbnd3  38897  sstotbnd  38901  prdsbnd  38919  cntotbnd  38922  heiborlem1  38937  heibor  38947  dihintcl  42593  focofob  48355