Theorem f1ofn 6803

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

Syntax hints:   → wi 4   Fn wfn 6512  –1-1-onto→wf1o 6516

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 209  df-an 400  df-f 6521  df-f1 6522  df-f1o 6524

This theorem is referenced by:  f1ofun  6804  f1odm  6806  f1odmOLD  6807  fveqf1o  7282  f1ofvswap  7286  isomin  7317  isoini  7318  isofrlem  7320  isoselem  7321  weniso  7334  bren  8933  enfixsn  9054  dif1enlem  9124  f1oenfi  9143  f1oenfirn  9144  f1domfi  9145  phplem2  9169  php3  9173  domunfican  9262  fiint  9267  supisolem  9417  ordiso2  9460  unxpwdom2  9533  wemapwe  9649  djuun  9881  infxpenlem  9966  ackbij2lem2  10192  ackbij2lem3  10193  fpwwe2lem8  10593  canthp1lem2  10608  hashfacen  14464  hashf1lem1  14465  fprodss  15961  phimullem  16797  unbenlem  16927  0ram  17039  symgfixelsi  19458  symgfixf1  19460  f1omvdmvd  19466  f1omvdcnv  19467  f1omvdconj  19469  f1otrspeq  19470  symggen  19493  psgnunilem1  19516  dprdf1o  20057  znleval  21586  znunithash  21596  mdetdiaglem  22638  basqtop  23751  tgqtop  23752  reghmph  23833  ordthmeolem  23841  qtophmeo  23857  imasf1oxmet  24415  imasf1omet  24416  imasf1obl  24528  imasf1oxms  24529  cnheiborlem  24996  ovolctb  25532  mbfimaopnlem  25697  logblog  26834  axcontlem5  29115  nvinvfval  30789  adjbd1o  32234  isoun  32854  fsumiunle  32981  indf1ofs  33005  symgcom  33224  pmtrcnel  33230  psgnfzto1stlem  33241  tocycfvres1  33251  tocycfvres2  33252  cycpmfvlem  33253  cycpmfv3  33256  cycpmconjvlem  33282  cycpmrn  33284  cycpmconjslem2  33296  1arithidomlem2  33693  esumiun  34352  eulerpartgbij  34630  eulerpartlemgh  34636  ballotlemsima  34774  vonf1owevOLD  35417  derangenlem  35485  subfacp1lem3  35496  subfacp1lem4  35497  subfacp1lem5  35498  fv1stcnv  36091  fv2ndcnv  36092  poimirlem1  38084  poimirlem2  38085  poimirlem3  38086  poimirlem4  38087  poimirlem6  38089  poimirlem7  38090  poimirlem8  38091  poimirlem9  38092  poimirlem13  38096  poimirlem14  38097  poimirlem15  38098  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem23  38106  ltrnid  40723  ltrneq2  40736  cdleme51finvN  41144  diaintclN  41646  dibintclN  41755  mapdcl  42241  kelac1  43604  gicabl  43640  brco2f1o  44572  brco3f1o  44573  ntrclsfv1  44595  ntrneifv1  44619  clsneikex  44646  clsneinex  44647  neicvgmex  44657  neicvgel1  44659  brpermmodel  45543  permaxpow  45549  permaxun  45551  permac8prim  45554  stoweidlem27  46565  3f1oss1  47633  uhgrimprop  48478  isuspgrimlem  48481  upgrimwlklem5  48487  gricushgr  48503  uhgrimisgrgric  48517  clnbgrgrimlem  48519  clnbgrgrim  48520  grtriclwlk3  48531  grimgrtri  48535  isubgr3stgrlem4  48555  isubgr3stgrlem7  48558  grlimprclnbgr  48582  grlimgrtrilem2  48588