Theorem f1ofn 6811

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

Syntax hints:   → wi 4   Fn wfn 6520  –1-1-onto→wf1o 6524

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 6529  df-f1 6530  df-f1o 6532

This theorem is referenced by:  f1ofun  6812  f1odm  6814  f1odmOLD  6815  fveqf1o  7290  f1ofvswap  7294  isomin  7325  isoini  7326  isofrlem  7328  isoselem  7329  weniso  7342  bren  8941  enfixsn  9062  dif1enlem  9132  f1oenfi  9151  f1oenfirn  9152  f1domfi  9153  phplem2  9177  php3  9181  domunfican  9269  fiint  9274  supisolem  9422  ordiso2  9465  unxpwdom2  9538  wemapwe  9654  djuun  9900  infxpenlem  9985  ackbij2lem2  10210  ackbij2lem3  10211  fpwwe2lem8  10611  canthp1lem2  10626  hashfacen  14479  hashf1lem1  14480  fprodss  15990  phimullem  16826  unbenlem  16956  0ram  17068  symgfixelsi  19493  symgfixf1  19495  f1omvdmvd  19501  f1omvdcnv  19502  f1omvdconj  19504  f1otrspeq  19505  symggen  19528  psgnunilem1  19551  dprdf1o  20092  znleval  21661  znunithash  21671  mdetdiaglem  22712  basqtop  23825  tgqtop  23826  reghmph  23907  ordthmeolem  23915  qtophmeo  23931  imasf1oxmet  24489  imasf1omet  24490  imasf1obl  24602  imasf1oxms  24603  cnheiborlem  25070  ovolctb  25606  mbfimaopnlem  25771  logblog  26911  axcontlem5  29223  nvinvfval  30897  adjbd1o  32342  isoun  32955  fsumiunle  33081  indf1ofs  33094  symgcom  33311  pmtrcnel  33317  psgnfzto1stlem  33328  tocycfvres1  33338  tocycfvres2  33339  cycpmfvlem  33340  cycpmfv3  33343  cycpmconjvlem  33369  cycpmrn  33371  cycpmconjslem2  33383  1arithidomlem2  33738  esumiun  34396  eulerpartgbij  34674  eulerpartlemgh  34680  ballotlemsima  34818  vonf1owevOLD  35460  derangenlem  35529  subfacp1lem3  35540  subfacp1lem4  35541  subfacp1lem5  35542  fv1stcnv  36135  fv2ndcnv  36136  poimirlem1  38127  poimirlem2  38128  poimirlem3  38129  poimirlem4  38130  poimirlem6  38132  poimirlem7  38133  poimirlem8  38134  poimirlem9  38135  poimirlem13  38139  poimirlem14  38140  poimirlem15  38141  poimirlem16  38142  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  poimirlem23  38149  ltrnid  40766  ltrneq2  40779  cdleme51finvN  41187  diaintclN  41689  dibintclN  41798  mapdcl  42284  kelac1  43647  gicabl  43683  brco2f1o  44615  brco3f1o  44616  ntrclsfv1  44638  ntrneifv1  44662  clsneikex  44689  clsneinex  44690  neicvgmex  44700  neicvgel1  44702  brpermmodel  45571  permaxpow  45577  permaxun  45579  permac8prim  45582  stoweidlem27  46600  3f1oss1  47668  uhgrimprop  48513  isuspgrimlem  48516  upgrimwlklem5  48522  gricushgr  48538  uhgrimisgrgric  48552  clnbgrgrimlem  48554  clnbgrgrim  48555  grtriclwlk3  48566  grimgrtri  48570  isubgr3stgrlem4  48590  isubgr3stgrlem7  48593  grlimprclnbgr  48617  grlimgrtrilem2  48623