Theorem dffn4 6749

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  ran crn 5622   Fn wfn 6484  –onto→wfo 6487

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 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-fo 6495

This theorem is referenced by:  funforn  6750  fimadmfo  6752  ffoss  7887  tposf2  8189  rneqdmfinf1o  9227  fidomdm  9228  indexfi  9254  intrnfi  9310  fifo  9326  ixpiunwdom  9486  infpwfien  9963  infmap2  10118  cfflb  10160  cfslb2n  10169  ttukeylem6  10415  dmct  10425  fnrndomg  10437  rankcf  10678  tskuni  10684  tskurn  10690  fseqsupcl  13894  s7f1o  14883  vdwlem6  16908  0ram2  16943  0ramcl  16945  quslem  17457  gsumval3  19829  gsumzoppg  19866  mplsubrglem  21951  rncmp  23321  cmpsub  23325  tgcmp  23326  hauscmplem  23331  conncn  23351  2ndcctbss  23380  2ndcomap  23383  2ndcsep  23384  comppfsc  23457  ptcnplem  23546  txtube  23565  txcmplem1  23566  tx1stc  23575  tx2ndc  23576  qtopid  23630  qtopcmplem  23632  qtopkgen  23635  kqtopon  23652  kqopn  23659  kqcld  23660  qtopf1  23741  rnelfm  23878  fmfnfmlem2  23880  fmfnfm  23883  alexsubALT  23976  ptcmplem2  23978  tmdgsum2  24021  tsmsxplem1  24078  met1stc  24446  met2ndci  24447  uniiccdif  25516  dyadmbl  25538  mbfimaopnlem  25593  i1fadd  25633  i1fmul  25634  i1fmulc  25641  mbfi1fseqlem4  25656  limciun  25832  aannenlem3  26275  efabl  26496  logccv  26609  locfinreflem  33864  mvrsfpw  35561  msrfo  35601  mtyf  35607  bj-inftyexpitaufo  37257  itg2addnclem2  37722  istotbnd3  37821  sstotbnd  37825  prdsbnd  37843  cntotbnd  37846  heiborlem1  37861  heibor  37871  dihintcl  41453  focofob  47194