Theorem f1ofn 6804

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

Syntax hints:   → wi 4   Fn wfn 6509  –1-1-onto→wf1o 6513

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 6518  df-f1 6519  df-f1o 6521

This theorem is referenced by:  f1ofun  6805  f1odm  6807  fveqf1o  7280  f1ofvswap  7284  isomin  7315  isoini  7316  isofrlem  7318  isoselem  7319  weniso  7332  bren  8931  enfixsn  9055  dif1enlem  9126  dif1enlemOLD  9127  f1oenfi  9149  f1oenfirn  9150  f1domfi  9151  phplem2  9175  php3  9179  domunfican  9279  fiint  9284  fiintOLD  9285  supisolem  9432  ordiso2  9475  unxpwdom2  9548  wemapwe  9657  djuun  9886  infxpenlem  9973  ackbij2lem2  10199  ackbij2lem3  10200  fpwwe2lem8  10598  canthp1lem2  10613  hashfacen  14426  hashf1lem1  14427  fprodss  15921  phimullem  16756  unbenlem  16886  0ram  16998  symgfixelsi  19372  symgfixf1  19374  f1omvdmvd  19380  f1omvdcnv  19381  f1omvdconj  19383  f1otrspeq  19384  symggen  19407  psgnunilem1  19430  dprdf1o  19971  znleval  21471  znunithash  21481  mdetdiaglem  22492  basqtop  23605  tgqtop  23606  reghmph  23687  ordthmeolem  23695  qtophmeo  23711  imasf1oxmet  24270  imasf1omet  24271  imasf1obl  24383  imasf1oxms  24384  cnheiborlem  24860  ovolctb  25398  mbfimaopnlem  25563  logblog  26709  axcontlem5  28902  nvinvfval  30576  adjbd1o  32021  isoun  32632  fsumiunle  32761  indf1ofs  32796  symgcom  33047  pmtrcnel  33053  psgnfzto1stlem  33064  tocycfvres1  33074  tocycfvres2  33075  cycpmfvlem  33076  cycpmfv3  33079  cycpmconjvlem  33105  cycpmrn  33107  cycpmconjslem2  33119  1arithidomlem2  33514  esumiun  34091  eulerpartgbij  34370  eulerpartlemgh  34376  ballotlemsima  34514  vonf1owev  35102  derangenlem  35165  subfacp1lem3  35176  subfacp1lem4  35177  subfacp1lem5  35178  fv1stcnv  35771  fv2ndcnv  35772  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem9  37630  poimirlem13  37634  poimirlem14  37635  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem23  37644  ltrnid  40136  ltrneq2  40149  cdleme51finvN  40557  diaintclN  41059  dibintclN  41168  mapdcl  41654  kelac1  43059  gicabl  43095  brco2f1o  44028  brco3f1o  44029  ntrclsfv1  44051  ntrneifv1  44075  clsneikex  44102  clsneinex  44103  neicvgmex  44113  neicvgel1  44115  brpermmodel  45000  permaxpow  45006  permaxun  45008  permac8prim  45011  stoweidlem27  46032  3f1oss1  47080  uhgrimprop  47896  isuspgrimlem  47899  upgrimwlklem5  47905  gricushgr  47921  uhgrimisgrgric  47935  clnbgrgrimlem  47937  clnbgrgrim  47938  grtriclwlk3  47948  grimgrtri  47952  isubgr3stgrlem4  47972  isubgr3stgrlem7  47975  grlimgrtrilem2  47998