Theorem dffn4 6746

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ran crn 5624   Fn wfn 6481  –onto→wfo 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fo 6492

This theorem is referenced by:  funforn  6747  fimadmfo  6749  ffoss  7888  tposf2  8190  rneqdmfinf1o  9242  fidomdm  9243  indexfi  9269  intrnfi  9325  fifo  9341  ixpiunwdom  9501  infpwfien  9975  infmap2  10130  cfflb  10172  cfslb2n  10181  ttukeylem6  10427  dmct  10437  fnrndomg  10449  rankcf  10690  tskuni  10696  tskurn  10702  fseqsupcl  13902  s7f1o  14891  vdwlem6  16916  0ram2  16951  0ramcl  16953  quslem  17465  gsumval3  19804  gsumzoppg  19841  mplsubrglem  21929  rncmp  23299  cmpsub  23303  tgcmp  23304  hauscmplem  23309  conncn  23329  2ndcctbss  23358  2ndcomap  23361  2ndcsep  23362  comppfsc  23435  ptcnplem  23524  txtube  23543  txcmplem1  23544  tx1stc  23553  tx2ndc  23554  qtopid  23608  qtopcmplem  23610  qtopkgen  23613  kqtopon  23630  kqopn  23637  kqcld  23638  qtopf1  23719  rnelfm  23856  fmfnfmlem2  23858  fmfnfm  23861  alexsubALT  23954  ptcmplem2  23956  tmdgsum2  23999  tsmsxplem1  24056  met1stc  24425  met2ndci  24426  uniiccdif  25495  dyadmbl  25517  mbfimaopnlem  25572  i1fadd  25612  i1fmul  25613  i1fmulc  25620  mbfi1fseqlem4  25635  limciun  25811  aannenlem3  26254  efabl  26475  logccv  26588  locfinreflem  33806  mvrsfpw  35478  msrfo  35518  mtyf  35524  bj-inftyexpitaufo  37175  itg2addnclem2  37651  istotbnd3  37750  sstotbnd  37754  prdsbnd  37772  cntotbnd  37775  heiborlem1  37790  heibor  37800  dihintcl  41323  focofob  47065