Theorem dffn4 6596

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

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1537  ran crn 5556   Fn wfn 6350  –onto→wfo 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-fo 6361

This theorem is referenced by:  funforn  6597  fimadmfo  6599  ffoss  7647  tposf2  7916  rneqdmfinf1o  8800  fidomdm  8801  pwfilem  8818  indexfi  8832  intrnfi  8880  fifo  8896  ixpiunwdom  9055  infpwfien  9488  infmap2  9640  cfflb  9681  cfslb2n  9690  ttukeylem6  9936  dmct  9946  fnrndomg  9958  rankcf  10199  tskuni  10205  tskurn  10211  fseqsupcl  13346  vdwlem6  16322  0ram2  16357  0ramcl  16359  quslem  16816  gsumval3  19027  gsumzoppg  19064  mplsubrglem  20219  rncmp  22004  cmpsub  22008  tgcmp  22009  hauscmplem  22014  conncn  22034  2ndcctbss  22063  2ndcomap  22066  2ndcsep  22067  comppfsc  22140  ptcnplem  22229  txtube  22248  txcmplem1  22249  tx1stc  22258  tx2ndc  22259  qtopid  22313  qtopcmplem  22315  qtopkgen  22318  kqtopon  22335  kqopn  22342  kqcld  22343  qtopf1  22424  rnelfm  22561  fmfnfmlem2  22563  fmfnfm  22566  alexsubALT  22659  ptcmplem2  22661  tmdgsum2  22704  tsmsxplem1  22761  met1stc  23131  met2ndci  23132  uniiccdif  24179  dyadmbl  24201  mbfimaopnlem  24256  i1fadd  24296  i1fmul  24297  itg1addlem4  24300  i1fmulc  24304  mbfi1fseqlem4  24319  limciun  24492  aannenlem3  24919  efabl  25134  logccv  25246  locfinreflem  31104  mvrsfpw  32753  msrfo  32793  mtyf  32799  bj-inftyexpitaufo  34487  itg2addnclem2  34959  istotbnd3  35064  sstotbnd  35068  prdsbnd  35086  cntotbnd  35089  heiborlem1  35104  heibor  35114  dihintcl  38495