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

Theorem dffn4 6078
 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 2621 . . 3 ran 𝐹 = ran 𝐹
21biantru 526 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3 df-fo 5853 . 2 (𝐹:𝐴onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
42, 3bitr4i 267 1 (𝐹 Fn 𝐴𝐹:𝐴onto→ran 𝐹)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1480  ran crn 5075   Fn wfn 5842  –onto→wfo 5845 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-fo 5853 This theorem is referenced by:  funforn  6079  ffoss  7074  tposf2  7321  mapsn  7843  rneqdmfinf1o  8186  fidomdm  8187  pwfilem  8204  indexfi  8218  intrnfi  8266  fifo  8282  ixpiunwdom  8440  infpwfien  8829  infmap2  8984  cfflb  9025  cfslb2n  9034  ttukeylem6  9280  dmct  9290  fnrndomg  9302  rankcf  9543  tskuni  9549  tskurn  9555  fseqsupcl  12716  vdwlem6  15614  0ram2  15649  0ramcl  15651  quslem  16124  gsumval3  18229  gsumzoppg  18265  mplsubrglem  19358  rncmp  21109  cmpsub  21113  tgcmp  21114  hauscmplem  21119  conncn  21139  2ndcctbss  21168  2ndcomap  21171  2ndcsep  21172  comppfsc  21245  ptcnplem  21334  txtube  21353  txcmplem1  21354  tx1stc  21363  tx2ndc  21364  qtopid  21418  qtopcmplem  21420  qtopkgen  21423  kqtopon  21440  kqopn  21447  kqcld  21448  qtopf1  21529  rnelfm  21667  fmfnfmlem2  21669  fmfnfm  21672  alexsubALT  21765  ptcmplem2  21767  tmdgsum2  21810  tsmsxplem1  21866  met1stc  22236  met2ndci  22237  uniiccdif  23252  dyadmbl  23274  mbfimaopnlem  23328  i1fadd  23368  i1fmul  23369  itg1addlem4  23372  i1fmulc  23376  mbfi1fseqlem4  23391  limciun  23564  aannenlem3  23989  efabl  24200  logccv  24309  locfinreflem  29686  mvrsfpw  31108  msrfo  31148  mtyf  31154  itg2addnclem2  33091  istotbnd3  33199  sstotbnd  33203  prdsbnd  33221  cntotbnd  33224  heiborlem1  33239  heibor  33249  dihintcl  36110  mapsnd  38859
 Copyright terms: Public domain W3C validator