Theorem dffn4 6802

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1569  ran crn 5651   Fn wfn 6533  –onto→wfo 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-fo 6544

This theorem is used by:  funforn  6803  fimadmfo  6805  ffoss  7958  tposf2  8267  rneqdmfinf1o  9322  fidomdm  9323  indexfi  9349  intrnfi  9408  fifo  9424  ixpiunwdom  9584  infpwfien  10141  infmap2  10295  cfflb  10337  cfslb2n  10346  ttukeylem6  10592  dmct  10602  dmctOLD  10603  imadomnum  10614  fnrndomnum  10617  fnrndomgOLD  10619  rankcf  10862  tskuni  10868  tskurn  10874  fseqsupcl  14120  s7f1o  15119  vdwlem6  17164  0ram2  17199  0ramcl  17201  quslem  17715  gsumval3  20121  gsumzoppg  20158  mplsubrglem  22311  rncmp  23714  cmpsub  23718  tgcmp  23719  hauscmplem  23724  conncn  23744  2ndcctbss  23774  2ndcomap  23777  2ndcsep  23778  comppfsc  23851  ptcnplem  23940  txtube  23959  txcmplem1  23960  tx1stc  23969  tx2ndc  23970  qtopid  24024  qtopcmplem  24026  qtopkgen  24029  kqtopon  24046  kqopn  24053  kqcld  24054  qtopf1  24135  rnelfm  24272  fmfnfmlem2  24274  fmfnfm  24277  alexsubALT  24370  ptcmplem2  24372  tmdgsum2  24415  tsmsxplem1  24472  met1stc  24840  met2ndci  24841  uniiccdif  25899  dyadmbl  25921  mbfimaopnlem  25976  i1fadd  26016  i1fmul  26017  i1fmulc  26024  mbfi1fseqlem4  26039  limciun  26214  aannenlem3  26657  efabl  26878  logccv  26991  locfinreflem  34514  mvrsfpw  36313  msrfo  36353  mtyf  36359  bj-inftyexpitaufo  38166  itg2addnclem2  38633  istotbnd3  38748  sstotbnd  38752  prdsbnd  38770  cntotbnd  38773  heiborlem1  38788  heibor  38798  dihintcl  42444  focofob  48193