Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dffn4 Structured version   Visualization version   GIF version

Theorem dffn4 6034
 Description: A function maps onto its range. (Contributed by NM, 10-May-1998.)
Assertion
Ref Expression
dffn4 (𝐹 Fn 𝐴𝐹:𝐴onto→ran 𝐹)

Proof of Theorem dffn4
StepHypRef Expression
1 eqid 2610 . . 3 ran 𝐹 = ran 𝐹
21biantru 525 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3 df-fo 5810 . 2 (𝐹:𝐴onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
42, 3bitr4i 266 1 (𝐹 Fn 𝐴𝐹:𝐴onto→ran 𝐹)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   = wceq 1475  ran crn 5039   Fn wfn 5799  –onto→wfo 5802 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603  df-fo 5810 This theorem is referenced by:  funforn  6035  ffoss  7020  tposf2  7263  mapsn  7785  rneqdmfinf1o  8127  fidomdm  8128  pwfilem  8143  indexfi  8157  intrnfi  8205  fifo  8221  ixpiunwdom  8379  infpwfien  8768  infmap2  8923  cfflb  8964  cfslb2n  8973  ttukeylem6  9219  fnrndomg  9239  rankcf  9478  tskuni  9484  tskurn  9490  fseqsupcl  12638  vdwlem6  15528  0ram2  15563  0ramcl  15565  quslem  16026  gsumval3  18131  gsumzoppg  18167  mplsubrglem  19260  rncmp  21009  cmpsub  21013  tgcmp  21014  hauscmplem  21019  concn  21039  2ndcctbss  21068  2ndcomap  21071  2ndcsep  21072  comppfsc  21145  ptcnplem  21234  txtube  21253  txcmplem1  21254  tx1stc  21263  tx2ndc  21264  qtopid  21318  qtopcmplem  21320  qtopkgen  21323  kqtopon  21340  kqopn  21347  kqcld  21348  qtopf1  21429  rnelfm  21567  fmfnfmlem2  21569  fmfnfm  21572  alexsubALT  21665  ptcmplem2  21667  tmdgsum2  21710  tsmsxplem1  21766  met1stc  22136  met2ndci  22137  uniiccdif  23152  dyadmbl  23174  mbfimaopnlem  23228  i1fadd  23268  i1fmul  23269  itg1addlem4  23272  i1fmulc  23276  mbfi1fseqlem4  23291  limciun  23464  aannenlem3  23889  efabl  24100  logccv  24209  dmct  28877  locfinreflem  29235  mvrsfpw  30657  msrfo  30697  mtyf  30703  itg2addnclem2  32632  istotbnd3  32740  sstotbnd  32744  prdsbnd  32762  cntotbnd  32765  heiborlem1  32780  heibor  32790  dihintcl  35651  mapsnd  38383
 Copyright terms: Public domain W3C validator