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

Theorem f1ofn 6176
 Description: A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1ofn (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)

Proof of Theorem f1ofn
StepHypRef Expression
1 f1of 6175 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2 ffn 6083 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   Fn wfn 5921  ⟶wf 5922  –1-1-onto→wf1o 5925 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 197  df-an 385  df-f 5930  df-f1 5931  df-f1o 5933 This theorem is referenced by:  f1ofun  6177  f1odm  6179  fveqf1o  6597  isomin  6627  isoini  6628  isofrlem  6630  isoselem  6631  weniso  6644  bren  8006  enfixsn  8110  phplem4  8183  php3  8187  domunfican  8274  fiint  8278  supisolem  8420  ordiso2  8461  unxpwdom2  8534  wemapwe  8632  infxpenlem  8874  ackbij2lem2  9100  ackbij2lem3  9101  fpwwe2lem9  9498  canthp1lem2  9513  hashfacen  13276  hashf1lem1  13277  fprodss  14722  phimullem  15531  unbenlem  15659  0ram  15771  symgfixelsi  17901  symgfixf1  17903  f1omvdmvd  17909  f1omvdcnv  17910  f1omvdconj  17912  f1otrspeq  17913  symggen  17936  psgnunilem1  17959  dprdf1o  18477  znleval  19951  znunithash  19961  mdetdiaglem  20452  basqtop  21562  tgqtop  21563  reghmph  21644  ordthmeolem  21652  qtophmeo  21668  imasf1oxmet  22227  imasf1omet  22228  imasf1obl  22340  imasf1oxms  22341  cnheiborlem  22800  ovolctb  23304  mbfimaopnlem  23467  logblog  24575  axcontlem5  25893  nvinvfval  27623  adjbd1o  29072  isoun  29607  fsumiunle  29703  psgnfzto1stlem  29978  indf1ofs  30216  esumiun  30284  eulerpartgbij  30562  eulerpartlemgh  30568  ballotlemsima  30705  derangenlem  31279  subfacp1lem3  31290  subfacp1lem4  31291  subfacp1lem5  31292  fv1stcnv  31804  fv2ndcnv  31805  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem9  33548  poimirlem13  33552  poimirlem14  33553  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem23  33562  ltrnid  35739  ltrneq2  35752  cdleme51finvN  36161  diaintclN  36664  dibintclN  36773  mapdcl  37259  kelac1  37950  gicabl  37986  brco2f1o  38647  brco3f1o  38648  ntrclsfv1  38670  ntrneifv1  38694  clsneikex  38721  clsneinex  38722  neicvgmex  38732  neicvgel1  38734  stoweidlem27  40562
 Copyright terms: Public domain W3C validator