Theorem dffn4 6159

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

Syntax hints:   ↔ wb 196   ∧ wa 383   = wceq 1523  ran crn 5144   Fn wfn 5921  –onto→wfo 5924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-fo 5932

This theorem is referenced by:  funforn  6160  ffoss  7169  tposf2  7421  mapsn  7941  rneqdmfinf1o  8283  fidomdm  8284  pwfilem  8301  indexfi  8315  intrnfi  8363  fifo  8379  ixpiunwdom  8537  infpwfien  8923  infmap2  9078  cfflb  9119  cfslb2n  9128  ttukeylem6  9374  dmct  9384  fnrndomg  9396  rankcf  9637  tskuni  9643  tskurn  9649  fseqsupcl  12816  vdwlem6  15737  0ram2  15772  0ramcl  15774  quslem  16250  gsumval3  18354  gsumzoppg  18390  mplsubrglem  19487  rncmp  21247  cmpsub  21251  tgcmp  21252  hauscmplem  21257  conncn  21277  2ndcctbss  21306  2ndcomap  21309  2ndcsep  21310  comppfsc  21383  ptcnplem  21472  txtube  21491  txcmplem1  21492  tx1stc  21501  tx2ndc  21502  qtopid  21556  qtopcmplem  21558  qtopkgen  21561  kqtopon  21578  kqopn  21585  kqcld  21586  qtopf1  21667  rnelfm  21804  fmfnfmlem2  21806  fmfnfm  21809  alexsubALT  21902  ptcmplem2  21904  tmdgsum2  21947  tsmsxplem1  22003  met1stc  22373  met2ndci  22374  uniiccdif  23392  dyadmbl  23414  mbfimaopnlem  23467  i1fadd  23507  i1fmul  23508  itg1addlem4  23511  i1fmulc  23515  mbfi1fseqlem4  23530  limciun  23703  aannenlem3  24130  efabl  24341  logccv  24454  locfinreflem  30035  mvrsfpw  31529  msrfo  31569  mtyf  31575  itg2addnclem2  33592  istotbnd3  33700  sstotbnd  33704  prdsbnd  33722  cntotbnd  33725  heiborlem1  33740  heibor  33750  dihintcl  36950  mapsnd  39702