Theorem f1ofn 6770

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 6769	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
2	1	ffnd 6658	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6482  –1-1-onto→wf1o 6486

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 6491  df-f1 6492  df-f1o 6494

This theorem is referenced by:  f1ofun  6771  f1odm  6773  fveqf1o  7246  f1ofvswap  7250  isomin  7281  isoini  7282  isofrlem  7284  isoselem  7285  weniso  7298  bren  8892  enfixsn  9013  dif1enlem  9083  f1oenfi  9102  f1oenfirn  9103  f1domfi  9104  phplem2  9128  php3  9132  domunfican  9221  fiint  9226  supisolem  9376  ordiso2  9419  unxpwdom2  9492  wemapwe  9607  djuun  9839  infxpenlem  9924  ackbij2lem2  10150  ackbij2lem3  10151  fpwwe2lem8  10550  canthp1lem2  10565  hashfacen  14405  hashf1lem1  14406  fprodss  15902  phimullem  16738  unbenlem  16868  0ram  16980  symgfixelsi  19399  symgfixf1  19401  f1omvdmvd  19407  f1omvdcnv  19408  f1omvdconj  19410  f1otrspeq  19411  symggen  19434  psgnunilem1  19457  dprdf1o  19998  znleval  21523  znunithash  21533  mdetdiaglem  22551  basqtop  23664  tgqtop  23665  reghmph  23746  ordthmeolem  23754  qtophmeo  23770  imasf1oxmet  24328  imasf1omet  24329  imasf1obl  24441  imasf1oxms  24442  cnheiborlem  24909  ovolctb  25445  mbfimaopnlem  25610  logblog  26744  axcontlem5  29025  nvinvfval  30699  adjbd1o  32144  isoun  32763  fsumiunle  32890  indf1ofs  32914  symgcom  33132  pmtrcnel  33138  psgnfzto1stlem  33149  tocycfvres1  33159  tocycfvres2  33160  cycpmfvlem  33161  cycpmfv3  33164  cycpmconjvlem  33190  cycpmrn  33192  cycpmconjslem2  33204  1arithidomlem2  33584  esumiun  34226  eulerpartgbij  34504  eulerpartlemgh  34510  ballotlemsima  34648  vonf1owev  35278  derangenlem  35341  subfacp1lem3  35352  subfacp1lem4  35353  subfacp1lem5  35354  fv1stcnv  35947  fv2ndcnv  35948  poimirlem1  37930  poimirlem2  37931  poimirlem3  37932  poimirlem4  37933  poimirlem6  37935  poimirlem7  37936  poimirlem8  37937  poimirlem9  37938  poimirlem13  37942  poimirlem14  37943  poimirlem15  37944  poimirlem16  37945  poimirlem17  37946  poimirlem19  37948  poimirlem20  37949  poimirlem23  37952  ltrnid  40569  ltrneq2  40582  cdleme51finvN  40990  diaintclN  41492  dibintclN  41601  mapdcl  42087  kelac1  43479  gicabl  43515  brco2f1o  44447  brco3f1o  44448  ntrclsfv1  44470  ntrneifv1  44494  clsneikex  44521  clsneinex  44522  neicvgmex  44532  neicvgel1  44534  brpermmodel  45418  permaxpow  45424  permaxun  45426  permac8prim  45429  stoweidlem27  46443  3f1oss1  47511  uhgrimprop  48356  isuspgrimlem  48359  upgrimwlklem5  48365  gricushgr  48381  uhgrimisgrgric  48395  clnbgrgrimlem  48397  clnbgrgrim  48398  grtriclwlk3  48409  grimgrtri  48413  isubgr3stgrlem4  48433  isubgr3stgrlem7  48436  grlimprclnbgr  48460  grlimgrtrilem2  48466