Theorem f1ofn 6621

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

Syntax hints:   → wi 4   Fn wfn 6334  –1-1-onto→wf1o 6338

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 400  df-f 6343  df-f1 6344  df-f1o 6346

This theorem is referenced by:  f1ofun  6622  f1odm  6624  fveqf1o  7072  f1ofvswap  7075  isomin  7105  isoini  7106  isofrlem  7108  isoselem  7109  weniso  7122  bren  8566  enfixsn  8677  phplem4  8751  php3  8755  dif1enlem  8761  f1oenfi  8781  f1oenfirn  8782  domunfican  8867  fiint  8871  supisolem  9012  ordiso2  9054  unxpwdom2  9127  wemapwe  9235  djuun  9430  infxpenlem  9515  ackbij2lem2  9742  ackbij2lem3  9743  fpwwe2lem8  10140  canthp1lem2  10155  hashfacen  13906  hashfacenOLD  13907  hashf1lem1  13908  hashf1lem1OLD  13909  fprodss  15396  phimullem  16218  unbenlem  16346  0ram  16458  symgfixelsi  18683  symgfixf1  18685  f1omvdmvd  18691  f1omvdcnv  18692  f1omvdconj  18694  f1otrspeq  18695  symggen  18718  psgnunilem1  18741  dprdf1o  19275  znleval  20375  znunithash  20385  mdetdiaglem  21351  basqtop  22464  tgqtop  22465  reghmph  22546  ordthmeolem  22554  qtophmeo  22570  imasf1oxmet  23130  imasf1omet  23131  imasf1obl  23243  imasf1oxms  23244  cnheiborlem  23708  ovolctb  24244  mbfimaopnlem  24409  logblog  25532  axcontlem5  26916  nvinvfval  28577  adjbd1o  30022  isoun  30611  fsumiunle  30720  symgcom  30931  pmtrcnel  30937  psgnfzto1stlem  30946  tocycfvres1  30956  tocycfvres2  30957  cycpmfvlem  30958  cycpmfv3  30961  cycpmconjvlem  30987  cycpmrn  30989  cycpmconjslem2  31001  indf1ofs  31566  esumiun  31634  eulerpartgbij  31911  eulerpartlemgh  31917  ballotlemsima  32054  derangenlem  32706  subfacp1lem3  32717  subfacp1lem4  32718  subfacp1lem5  32719  fv1stcnv  33327  fv2ndcnv  33328  poimirlem1  35423  poimirlem2  35424  poimirlem3  35425  poimirlem4  35426  poimirlem6  35428  poimirlem7  35429  poimirlem8  35430  poimirlem9  35431  poimirlem13  35435  poimirlem14  35436  poimirlem15  35437  poimirlem16  35438  poimirlem17  35439  poimirlem19  35441  poimirlem20  35442  poimirlem23  35445  ltrnid  37794  ltrneq2  37807  cdleme51finvN  38215  diaintclN  38717  dibintclN  38826  mapdcl  39312  kelac1  40482  gicabl  40518  brco2f1o  41210  brco3f1o  41211  ntrclsfv1  41233  ntrneifv1  41257  clsneikex  41284  clsneinex  41285  neicvgmex  41295  neicvgel1  41297  stoweidlem27  43132  isomushgr  44841  isomuspgrlem1  44842  isomuspgrlem2b  44844  isomuspgrlem2d  44846  isomuspgr  44849  isomgrtrlem  44853