Theorem f1ofn 6783

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

Syntax hints:   → wi 4   Fn wfn 6495  –1-1-onto→wf1o 6499

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 6504  df-f1 6505  df-f1o 6507

This theorem is referenced by:  f1ofun  6784  f1odm  6786  fveqf1o  7258  f1ofvswap  7262  isomin  7293  isoini  7294  isofrlem  7296  isoselem  7297  weniso  7310  bren  8905  enfixsn  9026  dif1enlem  9096  f1oenfi  9115  f1oenfirn  9116  f1domfi  9117  phplem2  9141  php3  9145  domunfican  9234  fiint  9239  supisolem  9389  ordiso2  9432  unxpwdom2  9505  wemapwe  9618  djuun  9850  infxpenlem  9935  ackbij2lem2  10161  ackbij2lem3  10162  fpwwe2lem8  10561  canthp1lem2  10576  hashfacen  14389  hashf1lem1  14390  fprodss  15883  phimullem  16718  unbenlem  16848  0ram  16960  symgfixelsi  19376  symgfixf1  19378  f1omvdmvd  19384  f1omvdcnv  19385  f1omvdconj  19387  f1otrspeq  19388  symggen  19411  psgnunilem1  19434  dprdf1o  19975  znleval  21521  znunithash  21531  mdetdiaglem  22554  basqtop  23667  tgqtop  23668  reghmph  23749  ordthmeolem  23757  qtophmeo  23773  imasf1oxmet  24331  imasf1omet  24332  imasf1obl  24444  imasf1oxms  24445  cnheiborlem  24921  ovolctb  25459  mbfimaopnlem  25624  logblog  26770  axcontlem5  29053  nvinvfval  30727  adjbd1o  32172  isoun  32791  fsumiunle  32920  indf1ofs  32958  symgcom  33176  pmtrcnel  33182  psgnfzto1stlem  33193  tocycfvres1  33203  tocycfvres2  33204  cycpmfvlem  33205  cycpmfv3  33208  cycpmconjvlem  33234  cycpmrn  33236  cycpmconjslem2  33248  1arithidomlem2  33628  esumiun  34271  eulerpartgbij  34549  eulerpartlemgh  34555  ballotlemsima  34693  vonf1owev  35321  derangenlem  35384  subfacp1lem3  35395  subfacp1lem4  35396  subfacp1lem5  35397  fv1stcnv  35990  fv2ndcnv  35991  poimirlem1  37869  poimirlem2  37870  poimirlem3  37871  poimirlem4  37872  poimirlem6  37874  poimirlem7  37875  poimirlem8  37876  poimirlem9  37877  poimirlem13  37881  poimirlem14  37882  poimirlem15  37883  poimirlem16  37884  poimirlem17  37885  poimirlem19  37887  poimirlem20  37888  poimirlem23  37891  ltrnid  40508  ltrneq2  40521  cdleme51finvN  40929  diaintclN  41431  dibintclN  41540  mapdcl  42026  kelac1  43417  gicabl  43453  brco2f1o  44385  brco3f1o  44386  ntrclsfv1  44408  ntrneifv1  44432  clsneikex  44459  clsneinex  44460  neicvgmex  44470  neicvgel1  44472  brpermmodel  45356  permaxpow  45362  permaxun  45364  permac8prim  45367  stoweidlem27  46382  3f1oss1  47432  uhgrimprop  48249  isuspgrimlem  48252  upgrimwlklem5  48258  gricushgr  48274  uhgrimisgrgric  48288  clnbgrgrimlem  48290  clnbgrgrim  48291  grtriclwlk3  48302  grimgrtri  48306  isubgr3stgrlem4  48326  isubgr3stgrlem7  48329  grlimprclnbgr  48353  grlimgrtrilem2  48359