Theorem f1ofn 6769

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

Syntax hints:   → wi 4   Fn wfn 6481  –1-1-onto→wf1o 6485

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 6490  df-f1 6491  df-f1o 6493

This theorem is referenced by:  f1ofun  6770  f1odm  6772  fveqf1o  7243  f1ofvswap  7247  isomin  7278  isoini  7279  isofrlem  7281  isoselem  7282  weniso  7295  bren  8889  enfixsn  9010  dif1enlem  9080  dif1enlemOLD  9081  f1oenfi  9103  f1oenfirn  9104  f1domfi  9105  phplem2  9129  php3  9133  domunfican  9230  fiint  9235  fiintOLD  9236  supisolem  9383  ordiso2  9426  unxpwdom2  9499  wemapwe  9612  djuun  9841  infxpenlem  9926  ackbij2lem2  10152  ackbij2lem3  10153  fpwwe2lem8  10551  canthp1lem2  10566  hashfacen  14379  hashf1lem1  14380  fprodss  15873  phimullem  16708  unbenlem  16838  0ram  16950  symgfixelsi  19332  symgfixf1  19334  f1omvdmvd  19340  f1omvdcnv  19341  f1omvdconj  19343  f1otrspeq  19344  symggen  19367  psgnunilem1  19390  dprdf1o  19931  znleval  21479  znunithash  21489  mdetdiaglem  22501  basqtop  23614  tgqtop  23615  reghmph  23696  ordthmeolem  23704  qtophmeo  23720  imasf1oxmet  24279  imasf1omet  24280  imasf1obl  24392  imasf1oxms  24393  cnheiborlem  24869  ovolctb  25407  mbfimaopnlem  25572  logblog  26718  axcontlem5  28931  nvinvfval  30602  adjbd1o  32047  isoun  32658  fsumiunle  32787  indf1ofs  32822  symgcom  33038  pmtrcnel  33044  psgnfzto1stlem  33055  tocycfvres1  33065  tocycfvres2  33066  cycpmfvlem  33067  cycpmfv3  33070  cycpmconjvlem  33096  cycpmrn  33098  cycpmconjslem2  33110  1arithidomlem2  33486  esumiun  34063  eulerpartgbij  34342  eulerpartlemgh  34348  ballotlemsima  34486  vonf1owev  35083  derangenlem  35146  subfacp1lem3  35157  subfacp1lem4  35158  subfacp1lem5  35159  fv1stcnv  35752  fv2ndcnv  35753  poimirlem1  37603  poimirlem2  37604  poimirlem3  37605  poimirlem4  37606  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem9  37611  poimirlem13  37615  poimirlem14  37616  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  poimirlem23  37625  ltrnid  40117  ltrneq2  40130  cdleme51finvN  40538  diaintclN  41040  dibintclN  41149  mapdcl  41635  kelac1  43039  gicabl  43075  brco2f1o  44008  brco3f1o  44009  ntrclsfv1  44031  ntrneifv1  44055  clsneikex  44082  clsneinex  44083  neicvgmex  44093  neicvgel1  44095  brpermmodel  44980  permaxpow  44986  permaxun  44988  permac8prim  44991  stoweidlem27  46012  3f1oss1  47063  uhgrimprop  47880  isuspgrimlem  47883  upgrimwlklem5  47889  gricushgr  47905  uhgrimisgrgric  47919  clnbgrgrimlem  47921  clnbgrgrim  47922  grtriclwlk3  47933  grimgrtri  47937  isubgr3stgrlem4  47957  isubgr3stgrlem7  47960  grlimprclnbgr  47984  grlimgrtrilem2  47990