Theorem dffn4 6798

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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1568  ran crn 5662   Fn wfn 6531  –onto→wfo 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-cleq 2753  df-fo 6542

This theorem is referenced by:  funforn  6799  fimadmfo  6801  ffoss  7942  tposf2  8245  rneqdmfinf1o  9289  fidomdm  9290  indexfi  9316  intrnfi  9375  fifo  9391  ixpiunwdom  9551  infpwfien  10045  infmap2  10199  cfflb  10242  cfslb2n  10251  ttukeylem6  10497  dmct  10507  fnrndomg  10519  rankcf  10761  tskuni  10767  tskurn  10773  fseqsupcl  14012  s7f1o  15002  vdwlem6  17045  0ram2  17080  0ramcl  17082  quslem  17596  gsumval3  19976  gsumzoppg  20013  mplsubrglem  22132  rncmp  23532  cmpsub  23536  tgcmp  23537  hauscmplem  23542  conncn  23562  2ndcctbss  23591  2ndcomap  23594  2ndcsep  23595  comppfsc  23668  ptcnplem  23757  txtube  23776  txcmplem1  23777  tx1stc  23786  tx2ndc  23787  qtopid  23841  qtopcmplem  23843  qtopkgen  23846  kqtopon  23863  kqopn  23870  kqcld  23871  qtopf1  23952  rnelfm  24089  fmfnfmlem2  24091  fmfnfm  24094  alexsubALT  24187  ptcmplem2  24189  tmdgsum2  24232  tsmsxplem1  24289  met1stc  24657  met2ndci  24658  uniiccdif  25716  dyadmbl  25738  mbfimaopnlem  25793  i1fadd  25833  i1fmul  25834  i1fmulc  25841  mbfi1fseqlem4  25856  limciun  26032  aannenlem3  26470  efabl  26691  logccv  26804  locfinreflem  34196  mvrsfpw  35952  msrfo  35992  mtyf  35998  bj-inftyexpitaufo  37790  itg2addnclem2  38267  istotbnd3  38366  sstotbnd  38370  prdsbnd  38388  cntotbnd  38391  heiborlem1  38406  heibor  38416  dihintcl  42064  focofob  47762