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

Theorem dffn4 6159
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 2651 . . 3 ran 𝐹 = ran 𝐹
21biantru 525 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3 df-fo 5932 . 2 (𝐹:𝐴onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
42, 3bitr4i 267 1 (𝐹 Fn 𝐴𝐹:𝐴onto→ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1523  ran crn 5144   Fn wfn 5921  ontowfo 5924
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-fo 5932
This theorem is referenced by:  funforn  6160  ffoss  7169  tposf2  7421  mapsn  7941  rneqdmfinf1o  8283  fidomdm  8284  pwfilem  8301  indexfi  8315  intrnfi  8363  fifo  8379  ixpiunwdom  8537  infpwfien  8923  infmap2  9078  cfflb  9119  cfslb2n  9128  ttukeylem6  9374  dmct  9384  fnrndomg  9396  rankcf  9637  tskuni  9643  tskurn  9649  fseqsupcl  12816  vdwlem6  15737  0ram2  15772  0ramcl  15774  quslem  16250  gsumval3  18354  gsumzoppg  18390  mplsubrglem  19487  rncmp  21247  cmpsub  21251  tgcmp  21252  hauscmplem  21257  conncn  21277  2ndcctbss  21306  2ndcomap  21309  2ndcsep  21310  comppfsc  21383  ptcnplem  21472  txtube  21491  txcmplem1  21492  tx1stc  21501  tx2ndc  21502  qtopid  21556  qtopcmplem  21558  qtopkgen  21561  kqtopon  21578  kqopn  21585  kqcld  21586  qtopf1  21667  rnelfm  21804  fmfnfmlem2  21806  fmfnfm  21809  alexsubALT  21902  ptcmplem2  21904  tmdgsum2  21947  tsmsxplem1  22003  met1stc  22373  met2ndci  22374  uniiccdif  23392  dyadmbl  23414  mbfimaopnlem  23467  i1fadd  23507  i1fmul  23508  itg1addlem4  23511  i1fmulc  23515  mbfi1fseqlem4  23530  limciun  23703  aannenlem3  24130  efabl  24341  logccv  24454  locfinreflem  30035  mvrsfpw  31529  msrfo  31569  mtyf  31575  itg2addnclem2  33592  istotbnd3  33700  sstotbnd  33704  prdsbnd  33722  cntotbnd  33725  heiborlem1  33740  heibor  33750  dihintcl  36950  mapsnd  39702
  Copyright terms: Public domain W3C validator