Theorem f1ofn 6775

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

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

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 208  df-an 397  df-f 6496  df-f1 6497  df-f1o 6499

This theorem is referenced by:  f1ofun  6776  f1odm  6778  fveqf1o  7253  f1ofvswap  7257  isomin  7288  isoini  7289  isofrlem  7291  isoselem  7292  weniso  7305  bren  8900  enfixsn  9021  dif1enlem  9091  f1oenfi  9110  f1oenfirn  9111  f1domfi  9112  phplem2  9136  php3  9140  domunfican  9229  fiint  9234  supisolem  9384  ordiso2  9427  unxpwdom2  9500  wemapwe  9616  djuun  9848  infxpenlem  9933  ackbij2lem2  10159  ackbij2lem3  10160  fpwwe2lem8  10559  canthp1lem2  10574  hashfacen  14414  hashf1lem1  14415  fprodss  15911  phimullem  16747  unbenlem  16877  0ram  16989  symgfixelsi  19408  symgfixf1  19410  f1omvdmvd  19416  f1omvdcnv  19417  f1omvdconj  19419  f1otrspeq  19420  symggen  19443  psgnunilem1  19466  dprdf1o  20007  znleval  21536  znunithash  21546  mdetdiaglem  22588  basqtop  23701  tgqtop  23702  reghmph  23783  ordthmeolem  23791  qtophmeo  23807  imasf1oxmet  24365  imasf1omet  24366  imasf1obl  24478  imasf1oxms  24479  cnheiborlem  24946  ovolctb  25482  mbfimaopnlem  25647  logblog  26781  axcontlem5  29062  nvinvfval  30736  adjbd1o  32181  isoun  32801  fsumiunle  32928  indf1ofs  32952  symgcom  33171  pmtrcnel  33177  psgnfzto1stlem  33188  tocycfvres1  33198  tocycfvres2  33199  cycpmfvlem  33200  cycpmfv3  33203  cycpmconjvlem  33229  cycpmrn  33231  cycpmconjslem2  33243  1arithidomlem2  33626  esumiun  34285  eulerpartgbij  34563  eulerpartlemgh  34569  ballotlemsima  34707  vonf1owev  35343  derangenlem  35406  subfacp1lem3  35417  subfacp1lem4  35418  subfacp1lem5  35419  fv1stcnv  36012  fv2ndcnv  36013  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem4  37998  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem9  38003  poimirlem13  38007  poimirlem14  38008  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem23  38017  ltrnid  40634  ltrneq2  40647  cdleme51finvN  41055  diaintclN  41557  dibintclN  41666  mapdcl  42152  kelac1  43515  gicabl  43551  brco2f1o  44483  brco3f1o  44484  ntrclsfv1  44506  ntrneifv1  44530  clsneikex  44557  clsneinex  44558  neicvgmex  44568  neicvgel1  44570  brpermmodel  45454  permaxpow  45460  permaxun  45462  permac8prim  45465  stoweidlem27  46477  3f1oss1  47545  uhgrimprop  48390  isuspgrimlem  48393  upgrimwlklem5  48399  gricushgr  48415  uhgrimisgrgric  48429  clnbgrgrimlem  48431  clnbgrgrim  48432  grtriclwlk3  48443  grimgrtri  48447  isubgr3stgrlem4  48467  isubgr3stgrlem7  48470  grlimprclnbgr  48494  grlimgrtrilem2  48500