Theorem f1ofn 6775

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

Step	Hyp	Ref	Expression
1		f1of 6774	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
2	1	ffnd 6663	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6487  –1-1-onto→wf1o 6491

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 207  df-an 396  df-f 6496  df-f1 6497  df-f1o 6499

This theorem is referenced by:  f1ofun  6776  f1odm  6778  fveqf1o  7248  f1ofvswap  7252  isomin  7283  isoini  7284  isofrlem  7286  isoselem  7287  weniso  7300  bren  8893  enfixsn  9014  dif1enlem  9084  f1oenfi  9103  f1oenfirn  9104  f1domfi  9105  phplem2  9129  php3  9133  domunfican  9222  fiint  9227  supisolem  9377  ordiso2  9420  unxpwdom2  9493  wemapwe  9606  djuun  9838  infxpenlem  9923  ackbij2lem2  10149  ackbij2lem3  10150  fpwwe2lem8  10549  canthp1lem2  10564  hashfacen  14377  hashf1lem1  14378  fprodss  15871  phimullem  16706  unbenlem  16836  0ram  16948  symgfixelsi  19364  symgfixf1  19366  f1omvdmvd  19372  f1omvdcnv  19373  f1omvdconj  19375  f1otrspeq  19376  symggen  19399  psgnunilem1  19422  dprdf1o  19963  znleval  21509  znunithash  21519  mdetdiaglem  22542  basqtop  23655  tgqtop  23656  reghmph  23737  ordthmeolem  23745  qtophmeo  23761  imasf1oxmet  24319  imasf1omet  24320  imasf1obl  24432  imasf1oxms  24433  cnheiborlem  24909  ovolctb  25447  mbfimaopnlem  25612  logblog  26758  axcontlem5  29041  nvinvfval  30715  adjbd1o  32160  isoun  32781  fsumiunle  32910  indf1ofs  32948  symgcom  33165  pmtrcnel  33171  psgnfzto1stlem  33182  tocycfvres1  33192  tocycfvres2  33193  cycpmfvlem  33194  cycpmfv3  33197  cycpmconjvlem  33223  cycpmrn  33225  cycpmconjslem2  33237  1arithidomlem2  33617  esumiun  34251  eulerpartgbij  34529  eulerpartlemgh  34535  ballotlemsima  34673  vonf1owev  35302  derangenlem  35365  subfacp1lem3  35376  subfacp1lem4  35377  subfacp1lem5  35378  fv1stcnv  35971  fv2ndcnv  35972  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem9  37830  poimirlem13  37834  poimirlem14  37835  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem23  37844  ltrnid  40395  ltrneq2  40408  cdleme51finvN  40816  diaintclN  41318  dibintclN  41427  mapdcl  41913  kelac1  43305  gicabl  43341  brco2f1o  44273  brco3f1o  44274  ntrclsfv1  44296  ntrneifv1  44320  clsneikex  44347  clsneinex  44348  neicvgmex  44358  neicvgel1  44360  brpermmodel  45244  permaxpow  45250  permaxun  45252  permac8prim  45255  stoweidlem27  46271  3f1oss1  47321  uhgrimprop  48138  isuspgrimlem  48141  upgrimwlklem5  48147  gricushgr  48163  uhgrimisgrgric  48177  clnbgrgrimlem  48179  clnbgrgrim  48180  grtriclwlk3  48191  grimgrtri  48195  isubgr3stgrlem4  48215  isubgr3stgrlem7  48218  grlimprclnbgr  48242  grlimgrtrilem2  48248