Theorem f1ofn 6828

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

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

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 6547  df-f1 6548  df-f1o 6550

This theorem is used by:  f1ofun  6829  f1odm  6831  f1odmOLD  6832  fveqf1o  7311  f1ofvswap  7315  isomin  7346  isoini  7347  isofrlem  7349  isoselem  7350  weniso  7365  bren  8962  enfixsn  9084  dif1enlem  9154  f1oenfi  9173  f1oenfirn  9174  f1domfi  9175  phplem2  9199  php3  9203  domunfican  9291  fiint  9296  supisolem  9444  ordiso2  9487  unxpwdom2  9560  wemapwe  9676  djuun  9931  infxpenlem  10016  ackbij2lem2  10241  ackbij2lem3  10242  fpwwe2lem8  10641  canthp1lem2  10656  hashfacen  14511  hashf1lem1  14512  fprodss  16028  phimullem  16863  unbenlem  16993  0ram  17105  symgfixelsi  19536  symgfixf1  19538  f1omvdmvd  19544  f1omvdcnv  19545  f1omvdconj  19547  f1otrspeq  19548  symggen  19571  psgnunilem1  19594  dprdf1o  20135  znleval  21741  znunithash  21751  mdetdiaglem  22792  basqtop  23905  tgqtop  23906  reghmph  23987  ordthmeolem  23995  qtophmeo  24011  imasf1oxmet  24569  imasf1omet  24570  imasf1obl  24682  imasf1oxms  24683  cnheiborlem  25150  ovolctb  25686  mbfimaopnlem  25851  logblog  26994  axcontlem5  29355  nvinvfval  31029  adjbd1o  32474  isoun  33084  fsumiunle  33210  indf1ofs  33223  symgcom  33434  pmtrcnel  33440  psgnfzto1stlem  33451  tocycfvres1  33461  tocycfvres2  33462  cycpmfvlem  33463  cycpmfv3  33466  cycpmconjvlem  33492  cycpmrn  33494  cycpmconjslem2  33506  1arithidomlem2  33857  esumiun  34515  eulerpartgbij  34794  eulerpartlemgh  34800  ballotlemsima  34938  vonf1owevOLD  35618  derangenlem  35684  subfacp1lem3  35695  subfacp1lem4  35696  subfacp1lem5  35697  fv1stcnv  36290  fv2ndcnv  36291  poimirlem1  38313  poimirlem2  38314  poimirlem3  38315  poimirlem4  38316  poimirlem6  38318  poimirlem7  38319  poimirlem8  38320  poimirlem9  38321  poimirlem13  38325  poimirlem14  38326  poimirlem15  38327  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem23  38335  ltrnid  40950  ltrneq2  40963  cdleme51finvN  41371  diaintclN  41873  dibintclN  41982  mapdcl  42468  kelac1  43831  gicabl  43867  brco2f1o  44799  brco3f1o  44800  ntrclsfv1  44822  ntrneifv1  44846  clsneikex  44873  clsneinex  44874  neicvgmex  44884  neicvgel1  44886  brpermmodel  45753  permaxpow  45759  permaxun  45761  permac8prim  45764  stoweidlem27  46782  3f1oss1  47853  uhgrimprop  48698  isuspgrimlem  48701  upgrimwlklem5  48707  gricushgr  48723  uhgrimisgrgric  48737  clnbgrgrimlem  48739  clnbgrgrim  48740  grtriclwlk3  48751  grimgrtri  48755  isubgr3stgrlem4  48775  isubgr3stgrlem7  48778  grlimprclnbgr  48802  grlimgrtrilem2  48808