Theorem f1ofn 6817

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6526  –1-1-onto→wf1o 6530

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6535  df-f1 6536  df-f1o 6538

This theorem is used by:  f1ofun  6818  f1odm  6820  f1odmOLD  6821  fveqf1o  7302  f1ofvswap  7306  isomin  7337  isoini  7338  isofrlem  7340  isoselem  7341  weniso  7356  bren  8967  enfixsn  9089  dif1enlem  9159  f1oenfi  9178  f1oenfirn  9179  f1domfi  9180  phplem2  9204  php3  9208  domunfican  9297  fiint  9302  supisolem  9450  ordiso2  9493  unxpwdom2  9566  wemapwe  9682  djuun  9988  infxpenlem  10073  ackbij2lem2  10298  ackbij2lem3  10299  fpwwe2lem8  10704  canthp1lem2  10719  hashfacen  14579  hashf1lem1  14580  fprodss  16095  phimullem  16936  unbenlem  17066  0ram  17178  symgfixelsi  19629  symgfixf1  19631  f1omvdmvd  19637  f1omvdcnv  19638  f1omvdconj  19640  f1otrspeq  19641  symggen  19664  psgnunilem1  19687  dprdf1o  20228  znleval  21840  znunithash  21850  mdetdiaglem  22893  basqtop  24010  tgqtop  24011  reghmph  24092  ordthmeolem  24100  qtophmeo  24116  imasf1oxmet  24674  imasf1omet  24675  imasf1obl  24787  imasf1oxms  24788  cnheiborlem  25255  ovolctb  25791  mbfimaopnlem  25956  logblog  27102  axcontlem5  29528  nvinvfval  31224  adjbd1o  32669  isoun  33277  fsumiunle  33402  indf1ofs  33415  symgcom  33626  pmtrcnel  33632  psgnfzto1stlem  33643  tocycfvres1  33653  tocycfvres2  33654  cycpmfvlem  33655  cycpmfv3  33658  cycpmconjvlem  33684  cycpmrn  33686  cycpmconjslem2  33698  1arithidomlem2  34050  esumiun  34708  eulerpartgbij  34987  eulerpartlemgh  34993  ballotlemsima  35131  vonf1owevOLD  35862  derangenlem  35905  subfacp1lem3  35916  subfacp1lem4  35917  subfacp1lem5  35918  fv1stcnv  36511  fv2ndcnv  36512  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem4  38510  poimirlem6  38512  poimirlem7  38513  poimirlem8  38514  poimirlem9  38515  poimirlem13  38519  poimirlem14  38520  poimirlem15  38521  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem23  38529  ltrnid  41160  ltrneq2  41173  cdleme51finvN  41581  diaintclN  42083  dibintclN  42192  mapdcl  42678  kelac1  44023  gicabl  44059  brco2f1o  44991  brco3f1o  44992  ntrclsfv1  45014  ntrneifv1  45038  clsneikex  45065  clsneinex  45066  neicvgmex  45076  neicvgel1  45078  brpermmodel  45945  permaxpow  45951  permaxun  45953  permac8prim  45956  stoweidlem27  46981  3f1oss1  48089  uhgrimprop  48934  isuspgrimlem  48937  upgrimwlklem5  48943  gricushgr  48959  uhgrimisgrgric  48973  clnbgrgrimlem  48975  clnbgrgrim  48976  grtriclwlk3  48987  grimgrtri  48991  isubgr3stgrlem4  49011  isubgr3stgrlem7  49014  grlimprclnbgr  49038  grlimgrtrilem2  49044