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  7250  f1ofvswap  7254  isomin  7285  isoini  7286  isofrlem  7288  isoselem  7289  weniso  7302  bren  8896  enfixsn  9017  dif1enlem  9087  f1oenfi  9106  f1oenfirn  9107  f1domfi  9108  phplem2  9132  php3  9136  domunfican  9225  fiint  9230  supisolem  9380  ordiso2  9423  unxpwdom2  9496  wemapwe  9609  djuun  9841  infxpenlem  9926  ackbij2lem2  10152  ackbij2lem3  10153  fpwwe2lem8  10552  canthp1lem2  10567  hashfacen  14407  hashf1lem1  14408  fprodss  15904  phimullem  16740  unbenlem  16870  0ram  16982  symgfixelsi  19401  symgfixf1  19403  f1omvdmvd  19409  f1omvdcnv  19410  f1omvdconj  19412  f1otrspeq  19413  symggen  19436  psgnunilem1  19459  dprdf1o  20000  znleval  21544  znunithash  21554  mdetdiaglem  22573  basqtop  23686  tgqtop  23687  reghmph  23768  ordthmeolem  23776  qtophmeo  23792  imasf1oxmet  24350  imasf1omet  24351  imasf1obl  24463  imasf1oxms  24464  cnheiborlem  24931  ovolctb  25467  mbfimaopnlem  25632  logblog  26769  axcontlem5  29051  nvinvfval  30726  adjbd1o  32171  isoun  32790  fsumiunle  32917  indf1ofs  32941  symgcom  33159  pmtrcnel  33165  psgnfzto1stlem  33176  tocycfvres1  33186  tocycfvres2  33187  cycpmfvlem  33188  cycpmfv3  33191  cycpmconjvlem  33217  cycpmrn  33219  cycpmconjslem2  33231  1arithidomlem2  33611  esumiun  34254  eulerpartgbij  34532  eulerpartlemgh  34538  ballotlemsima  34676  vonf1owev  35306  derangenlem  35369  subfacp1lem3  35380  subfacp1lem4  35381  subfacp1lem5  35382  fv1stcnv  35975  fv2ndcnv  35976  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem9  37964  poimirlem13  37968  poimirlem14  37969  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem23  37978  ltrnid  40595  ltrneq2  40608  cdleme51finvN  41016  diaintclN  41518  dibintclN  41627  mapdcl  42113  kelac1  43509  gicabl  43545  brco2f1o  44477  brco3f1o  44478  ntrclsfv1  44500  ntrneifv1  44524  clsneikex  44551  clsneinex  44552  neicvgmex  44562  neicvgel1  44564  brpermmodel  45448  permaxpow  45454  permaxun  45456  permac8prim  45459  stoweidlem27  46473  3f1oss1  47535  uhgrimprop  48380  isuspgrimlem  48383  upgrimwlklem5  48389  gricushgr  48405  uhgrimisgrgric  48419  clnbgrgrimlem  48421  clnbgrgrim  48422  grtriclwlk3  48433  grimgrtri  48437  isubgr3stgrlem4  48457  isubgr3stgrlem7  48460  grlimprclnbgr  48484  grlimgrtrilem2  48490