Theorem f1ofn 6823

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

Syntax hints:   → wi 4   Fn wfn 6533  –1-1-onto→wf1o 6537

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 210  df-an 401  df-f 6542  df-f1 6543  df-f1o 6545

This theorem is referenced by:  f1ofun  6824  f1odm  6826  f1odmOLD  6827  fveqf1o  7302  f1ofvswap  7306  isomin  7337  isoini  7338  isofrlem  7340  isoselem  7341  weniso  7354  bren  8954  enfixsn  9075  dif1enlem  9145  f1oenfi  9164  f1oenfirn  9165  f1domfi  9166  phplem2  9190  php3  9194  domunfican  9282  fiint  9287  supisolem  9435  ordiso2  9478  unxpwdom2  9551  wemapwe  9667  djuun  9913  infxpenlem  9998  ackbij2lem2  10223  ackbij2lem3  10224  fpwwe2lem8  10624  canthp1lem2  10639  hashfacen  14493  hashf1lem1  14494  fprodss  16004  phimullem  16839  unbenlem  16969  0ram  17081  symgfixelsi  19506  symgfixf1  19508  f1omvdmvd  19514  f1omvdcnv  19515  f1omvdconj  19517  f1otrspeq  19518  symggen  19541  psgnunilem1  19564  dprdf1o  20105  znleval  21685  znunithash  21695  mdetdiaglem  22736  basqtop  23849  tgqtop  23850  reghmph  23931  ordthmeolem  23939  qtophmeo  23955  imasf1oxmet  24513  imasf1omet  24514  imasf1obl  24626  imasf1oxms  24627  cnheiborlem  25094  ovolctb  25630  mbfimaopnlem  25795  logblog  26938  axcontlem5  29299  nvinvfval  30973  adjbd1o  32418  isoun  33028  fsumiunle  33154  indf1ofs  33167  symgcom  33384  pmtrcnel  33390  psgnfzto1stlem  33401  tocycfvres1  33411  tocycfvres2  33412  cycpmfvlem  33413  cycpmfv3  33416  cycpmconjvlem  33442  cycpmrn  33444  cycpmconjslem2  33456  1arithidomlem2  33807  esumiun  34465  eulerpartgbij  34743  eulerpartlemgh  34749  ballotlemsima  34887  vonf1owevOLD  35575  derangenlem  35644  subfacp1lem3  35655  subfacp1lem4  35656  subfacp1lem5  35657  fv1stcnv  36250  fv2ndcnv  36251  poimirlem1  38253  poimirlem2  38254  poimirlem3  38255  poimirlem4  38256  poimirlem6  38258  poimirlem7  38259  poimirlem8  38260  poimirlem9  38261  poimirlem13  38265  poimirlem14  38266  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  poimirlem23  38275  ltrnid  40890  ltrneq2  40903  cdleme51finvN  41311  diaintclN  41813  dibintclN  41922  mapdcl  42408  kelac1  43773  gicabl  43809  brco2f1o  44741  brco3f1o  44742  ntrclsfv1  44764  ntrneifv1  44788  clsneikex  44815  clsneinex  44816  neicvgmex  44826  neicvgel1  44828  brpermmodel  45695  permaxpow  45701  permaxun  45703  permac8prim  45706  stoweidlem27  46724  3f1oss1  47795  uhgrimprop  48640  isuspgrimlem  48643  upgrimwlklem5  48649  gricushgr  48665  uhgrimisgrgric  48679  clnbgrgrimlem  48681  clnbgrgrim  48682  grtriclwlk3  48693  grimgrtri  48697  isubgr3stgrlem4  48717  isubgr3stgrlem7  48720  grlimprclnbgr  48744  grlimgrtrilem2  48750