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

Theorem dffn4 6578
 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 2822 . . 3 ran 𝐹 = ran 𝐹
21biantru 533 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3 df-fo 6340 . 2 (𝐹:𝐴onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
42, 3bitr4i 281 1 (𝐹 Fn 𝐴𝐹:𝐴onto→ran 𝐹)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ran crn 5533   Fn wfn 6329  –onto→wfo 6332 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815  df-fo 6340 This theorem is referenced by:  funforn  6579  fimadmfo  6581  ffoss  7633  tposf2  7903  rneqdmfinf1o  8788  fidomdm  8789  pwfilem  8806  indexfi  8820  intrnfi  8868  fifo  8884  ixpiunwdom  9042  infpwfien  9477  infmap2  9629  cfflb  9670  cfslb2n  9679  ttukeylem6  9925  dmct  9935  fnrndomg  9947  rankcf  10188  tskuni  10194  tskurn  10200  fseqsupcl  13340  vdwlem6  16311  0ram2  16346  0ramcl  16348  quslem  16807  gsumval3  19018  gsumzoppg  19055  mplsubrglem  20675  rncmp  21999  cmpsub  22003  tgcmp  22004  hauscmplem  22009  conncn  22029  2ndcctbss  22058  2ndcomap  22061  2ndcsep  22062  comppfsc  22135  ptcnplem  22224  txtube  22243  txcmplem1  22244  tx1stc  22253  tx2ndc  22254  qtopid  22308  qtopcmplem  22310  qtopkgen  22313  kqtopon  22330  kqopn  22337  kqcld  22338  qtopf1  22419  rnelfm  22556  fmfnfmlem2  22558  fmfnfm  22561  alexsubALT  22654  ptcmplem2  22656  tmdgsum2  22699  tsmsxplem1  22756  met1stc  23126  met2ndci  23127  uniiccdif  24180  dyadmbl  24202  mbfimaopnlem  24257  i1fadd  24297  i1fmul  24298  itg1addlem4  24301  i1fmulc  24305  mbfi1fseqlem4  24320  limciun  24495  aannenlem3  24924  efabl  25140  logccv  25252  locfinreflem  31162  mvrsfpw  32827  msrfo  32867  mtyf  32873  bj-inftyexpitaufo  34578  itg2addnclem2  35067  istotbnd3  35167  sstotbnd  35171  prdsbnd  35189  cntotbnd  35192  heiborlem1  35207  heibor  35217  dihintcl  38598
 Copyright terms: Public domain W3C validator