Theorem f1ofn 6771

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

Syntax hints:   → wi 4   Fn wfn 6483  –1-1-onto→wf1o 6487

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 6492  df-f1 6493  df-f1o 6495

This theorem is referenced by:  f1ofun  6772  f1odm  6774  fveqf1o  7244  f1ofvswap  7248  isomin  7279  isoini  7280  isofrlem  7282  isoselem  7283  weniso  7296  bren  8887  enfixsn  9008  dif1enlem  9078  f1oenfi  9097  f1oenfirn  9098  f1domfi  9099  phplem2  9123  php3  9127  domunfican  9215  fiint  9220  supisolem  9367  ordiso2  9410  unxpwdom2  9483  wemapwe  9596  djuun  9828  infxpenlem  9913  ackbij2lem2  10139  ackbij2lem3  10140  fpwwe2lem8  10538  canthp1lem2  10553  hashfacen  14365  hashf1lem1  14366  fprodss  15859  phimullem  16694  unbenlem  16824  0ram  16936  symgfixelsi  19351  symgfixf1  19353  f1omvdmvd  19359  f1omvdcnv  19360  f1omvdconj  19362  f1otrspeq  19363  symggen  19386  psgnunilem1  19409  dprdf1o  19950  znleval  21495  znunithash  21505  mdetdiaglem  22516  basqtop  23629  tgqtop  23630  reghmph  23711  ordthmeolem  23719  qtophmeo  23735  imasf1oxmet  24293  imasf1omet  24294  imasf1obl  24406  imasf1oxms  24407  cnheiborlem  24883  ovolctb  25421  mbfimaopnlem  25586  logblog  26732  axcontlem5  28950  nvinvfval  30624  adjbd1o  32069  isoun  32689  fsumiunle  32819  indf1ofs  32856  symgcom  33061  pmtrcnel  33067  psgnfzto1stlem  33078  tocycfvres1  33088  tocycfvres2  33089  cycpmfvlem  33090  cycpmfv3  33093  cycpmconjvlem  33119  cycpmrn  33121  cycpmconjslem2  33133  1arithidomlem2  33510  esumiun  34130  eulerpartgbij  34408  eulerpartlemgh  34414  ballotlemsima  34552  vonf1owev  35175  derangenlem  35238  subfacp1lem3  35249  subfacp1lem4  35250  subfacp1lem5  35251  fv1stcnv  35844  fv2ndcnv  35845  poimirlem1  37684  poimirlem2  37685  poimirlem3  37686  poimirlem4  37687  poimirlem6  37689  poimirlem7  37690  poimirlem8  37691  poimirlem9  37692  poimirlem13  37696  poimirlem14  37697  poimirlem15  37698  poimirlem16  37699  poimirlem17  37700  poimirlem19  37702  poimirlem20  37703  poimirlem23  37706  ltrnid  40257  ltrneq2  40270  cdleme51finvN  40678  diaintclN  41180  dibintclN  41289  mapdcl  41775  kelac1  43183  gicabl  43219  brco2f1o  44152  brco3f1o  44153  ntrclsfv1  44175  ntrneifv1  44199  clsneikex  44226  clsneinex  44227  neicvgmex  44237  neicvgel1  44239  brpermmodel  45123  permaxpow  45129  permaxun  45131  permac8prim  45134  stoweidlem27  46152  3f1oss1  47202  uhgrimprop  48019  isuspgrimlem  48022  upgrimwlklem5  48028  gricushgr  48044  uhgrimisgrgric  48058  clnbgrgrimlem  48060  clnbgrgrim  48061  grtriclwlk3  48072  grimgrtri  48076  isubgr3stgrlem4  48096  isubgr3stgrlem7  48099  grlimprclnbgr  48123  grlimgrtrilem2  48129