Theorem f1ofn 6618

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

Syntax hints:   → wi 4   Fn wfn 6352  –1-1-onto→wf1o 6356

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 399  df-f 6361  df-f1 6362  df-f1o 6364

This theorem is referenced by:  f1ofun  6619  f1odm  6621  fveqf1o  7060  isomin  7092  isoini  7093  isofrlem  7095  isoselem  7096  weniso  7109  bren  8520  enfixsn  8628  phplem4  8701  php3  8705  domunfican  8793  fiint  8797  supisolem  8939  ordiso2  8981  unxpwdom2  9054  wemapwe  9162  djuun  9357  infxpenlem  9441  ackbij2lem2  9664  ackbij2lem3  9665  fpwwe2lem9  10062  canthp1lem2  10077  hashfacen  13815  hashf1lem1  13816  fprodss  15304  phimullem  16118  unbenlem  16246  0ram  16358  symgfixelsi  18565  symgfixf1  18567  f1omvdmvd  18573  f1omvdcnv  18574  f1omvdconj  18576  f1otrspeq  18577  symggen  18600  psgnunilem1  18623  dprdf1o  19156  znleval  20703  znunithash  20713  mdetdiaglem  21209  basqtop  22321  tgqtop  22322  reghmph  22403  ordthmeolem  22411  qtophmeo  22427  imasf1oxmet  22987  imasf1omet  22988  imasf1obl  23100  imasf1oxms  23101  cnheiborlem  23560  ovolctb  24093  mbfimaopnlem  24258  logblog  25372  axcontlem5  26756  nvinvfval  28419  adjbd1o  29864  isoun  30439  fsumiunle  30547  symgcom  30729  pmtrcnel  30735  psgnfzto1stlem  30744  tocycfvres1  30754  tocycfvres2  30755  cycpmfvlem  30756  cycpmfv3  30759  cycpmconjvlem  30785  cycpmrn  30787  cycpmconjslem2  30799  indf1ofs  31287  esumiun  31355  eulerpartgbij  31632  eulerpartlemgh  31638  ballotlemsima  31775  derangenlem  32420  subfacp1lem3  32431  subfacp1lem4  32432  subfacp1lem5  32433  fv1stcnv  33022  fv2ndcnv  33023  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem9  34903  poimirlem13  34907  poimirlem14  34908  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem23  34917  ltrnid  37273  ltrneq2  37286  cdleme51finvN  37694  diaintclN  38196  dibintclN  38305  mapdcl  38791  kelac1  39670  gicabl  39706  brco2f1o  40389  brco3f1o  40390  ntrclsfv1  40412  ntrneifv1  40436  clsneikex  40463  clsneinex  40464  neicvgmex  40474  neicvgel1  40476  stoweidlem27  42319  isomushgr  43998  isomuspgrlem1  43999  isomuspgrlem2b  44001  isomuspgrlem2d  44003  isomuspgr  44006  isomgrtrlem  44010