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

Theorem dffn4 6262
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 2771 . . 3 ran 𝐹 = ran 𝐹
21biantru 519 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3 df-fo 6037 . 2 (𝐹:𝐴onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
42, 3bitr4i 267 1 (𝐹 Fn 𝐴𝐹:𝐴onto→ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382   = wceq 1631  ran crn 5250   Fn wfn 6026  ontowfo 6029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-fo 6037
This theorem is referenced by:  funforn  6263  ffoss  7274  tposf2  7528  mapsnd  8051  rneqdmfinf1o  8398  fidomdm  8399  pwfilem  8416  indexfi  8430  intrnfi  8478  fifo  8494  ixpiunwdom  8652  infpwfien  9085  infmap2  9242  cfflb  9283  cfslb2n  9292  ttukeylem6  9538  dmct  9548  fnrndomg  9560  rankcf  9801  tskuni  9807  tskurn  9813  fseqsupcl  12984  vdwlem6  15897  0ram2  15932  0ramcl  15934  quslem  16411  gsumval3  18515  gsumzoppg  18551  mplsubrglem  19654  rncmp  21420  cmpsub  21424  tgcmp  21425  hauscmplem  21430  conncn  21450  2ndcctbss  21479  2ndcomap  21482  2ndcsep  21483  comppfsc  21556  ptcnplem  21645  txtube  21664  txcmplem1  21665  tx1stc  21674  tx2ndc  21675  qtopid  21729  qtopcmplem  21731  qtopkgen  21734  kqtopon  21751  kqopn  21758  kqcld  21759  qtopf1  21840  rnelfm  21977  fmfnfmlem2  21979  fmfnfm  21982  alexsubALT  22075  ptcmplem2  22077  tmdgsum2  22120  tsmsxplem1  22176  met1stc  22546  met2ndci  22547  uniiccdif  23566  dyadmbl  23588  mbfimaopnlem  23642  i1fadd  23682  i1fmul  23683  itg1addlem4  23686  i1fmulc  23690  mbfi1fseqlem4  23705  limciun  23878  aannenlem3  24305  efabl  24517  logccv  24630  locfinreflem  30247  mvrsfpw  31741  msrfo  31781  mtyf  31787  itg2addnclem2  33794  istotbnd3  33902  sstotbnd  33906  prdsbnd  33924  cntotbnd  33927  heiborlem1  33942  heibor  33952  dihintcl  37154
  Copyright terms: Public domain W3C validator