Theorem dffn4 6750

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ran crn 5623   Fn wfn 6485  –onto→wfo 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  funforn  6751  fimadmfo  6753  ffoss  7890  tposf2  8191  rneqdmfinf1o  9234  fidomdm  9235  indexfi  9261  intrnfi  9320  fifo  9336  ixpiunwdom  9496  infpwfien  9973  infmap2  10128  cfflb  10170  cfslb2n  10179  ttukeylem6  10425  dmct  10435  fnrndomg  10447  rankcf  10689  tskuni  10695  tskurn  10701  fseqsupcl  13901  s7f1o  14890  vdwlem6  16915  0ram2  16950  0ramcl  16952  quslem  17465  gsumval3  19840  gsumzoppg  19877  mplsubrglem  21960  rncmp  23339  cmpsub  23343  tgcmp  23344  hauscmplem  23349  conncn  23369  2ndcctbss  23398  2ndcomap  23401  2ndcsep  23402  comppfsc  23475  ptcnplem  23564  txtube  23583  txcmplem1  23584  tx1stc  23593  tx2ndc  23594  qtopid  23648  qtopcmplem  23650  qtopkgen  23653  kqtopon  23670  kqopn  23677  kqcld  23678  qtopf1  23759  rnelfm  23896  fmfnfmlem2  23898  fmfnfm  23901  alexsubALT  23994  ptcmplem2  23996  tmdgsum2  24039  tsmsxplem1  24096  met1stc  24464  met2ndci  24465  uniiccdif  25523  dyadmbl  25545  mbfimaopnlem  25600  i1fadd  25640  i1fmul  25641  i1fmulc  25648  mbfi1fseqlem4  25663  limciun  25839  aannenlem3  26278  efabl  26499  logccv  26612  locfinreflem  33990  mvrsfpw  35694  msrfo  35734  mtyf  35740  bj-inftyexpitaufo  37514  itg2addnclem2  37984  istotbnd3  38083  sstotbnd  38087  prdsbnd  38105  cntotbnd  38108  heiborlem1  38123  heibor  38133  dihintcl  41781  focofob  47514