Theorem dffn4 6826

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 6567	. 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 5686   Fn wfn 6556  –onto→wfo 6559

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  funforn  6827  fimadmfo  6829  ffoss  7970  tposf2  8275  rneqdmfinf1o  9373  fidomdm  9374  indexfi  9400  intrnfi  9456  fifo  9472  ixpiunwdom  9630  infpwfien  10102  infmap2  10257  cfflb  10299  cfslb2n  10308  ttukeylem6  10554  dmct  10564  fnrndomg  10576  rankcf  10817  tskuni  10823  tskurn  10829  fseqsupcl  14018  s7f1o  15005  vdwlem6  17024  0ram2  17059  0ramcl  17061  quslem  17588  gsumval3  19925  gsumzoppg  19962  mplsubrglem  22024  rncmp  23404  cmpsub  23408  tgcmp  23409  hauscmplem  23414  conncn  23434  2ndcctbss  23463  2ndcomap  23466  2ndcsep  23467  comppfsc  23540  ptcnplem  23629  txtube  23648  txcmplem1  23649  tx1stc  23658  tx2ndc  23659  qtopid  23713  qtopcmplem  23715  qtopkgen  23718  kqtopon  23735  kqopn  23742  kqcld  23743  qtopf1  23824  rnelfm  23961  fmfnfmlem2  23963  fmfnfm  23966  alexsubALT  24059  ptcmplem2  24061  tmdgsum2  24104  tsmsxplem1  24161  met1stc  24534  met2ndci  24535  uniiccdif  25613  dyadmbl  25635  mbfimaopnlem  25690  i1fadd  25730  i1fmul  25731  i1fmulc  25738  mbfi1fseqlem4  25753  limciun  25929  aannenlem3  26372  efabl  26592  logccv  26705  locfinreflem  33839  mvrsfpw  35511  msrfo  35551  mtyf  35557  bj-inftyexpitaufo  37203  itg2addnclem2  37679  istotbnd3  37778  sstotbnd  37782  prdsbnd  37800  cntotbnd  37803  heiborlem1  37818  heibor  37828  dihintcl  41346  focofob  47092