Theorem dffn4 6781

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 2730	. . 3 ⊢ ran 𝐹 = ran 𝐹
2	1	biantru 529	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3		df-fo 6520	. 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 5642   Fn wfn 6509  –onto→wfo 6512

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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  funforn  6782  fimadmfo  6784  ffoss  7927  tposf2  8232  rneqdmfinf1o  9291  fidomdm  9292  indexfi  9318  intrnfi  9374  fifo  9390  ixpiunwdom  9550  infpwfien  10022  infmap2  10177  cfflb  10219  cfslb2n  10228  ttukeylem6  10474  dmct  10484  fnrndomg  10496  rankcf  10737  tskuni  10743  tskurn  10749  fseqsupcl  13949  s7f1o  14939  vdwlem6  16964  0ram2  16999  0ramcl  17001  quslem  17513  gsumval3  19844  gsumzoppg  19881  mplsubrglem  21920  rncmp  23290  cmpsub  23294  tgcmp  23295  hauscmplem  23300  conncn  23320  2ndcctbss  23349  2ndcomap  23352  2ndcsep  23353  comppfsc  23426  ptcnplem  23515  txtube  23534  txcmplem1  23535  tx1stc  23544  tx2ndc  23545  qtopid  23599  qtopcmplem  23601  qtopkgen  23604  kqtopon  23621  kqopn  23628  kqcld  23629  qtopf1  23710  rnelfm  23847  fmfnfmlem2  23849  fmfnfm  23852  alexsubALT  23945  ptcmplem2  23947  tmdgsum2  23990  tsmsxplem1  24047  met1stc  24416  met2ndci  24417  uniiccdif  25486  dyadmbl  25508  mbfimaopnlem  25563  i1fadd  25603  i1fmul  25604  i1fmulc  25611  mbfi1fseqlem4  25626  limciun  25802  aannenlem3  26245  efabl  26466  logccv  26579  locfinreflem  33837  mvrsfpw  35500  msrfo  35540  mtyf  35546  bj-inftyexpitaufo  37197  itg2addnclem2  37673  istotbnd3  37772  sstotbnd  37776  prdsbnd  37794  cntotbnd  37797  heiborlem1  37812  heibor  37822  dihintcl  41345  focofob  47085