Theorem f1ofn 6591

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

Syntax hints:   → wi 4   Fn wfn 6319  –1-1-onto→wf1o 6323

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 6328  df-f1 6329  df-f1o 6331

This theorem is referenced by:  f1ofun  6592  f1odm  6594  fveqf1o  7037  isomin  7069  isoini  7070  isofrlem  7072  isoselem  7073  weniso  7086  bren  8501  enfixsn  8609  phplem4  8683  php3  8687  domunfican  8775  fiint  8779  supisolem  8921  ordiso2  8963  unxpwdom2  9036  wemapwe  9144  djuun  9339  infxpenlem  9424  ackbij2lem2  9651  ackbij2lem3  9652  fpwwe2lem9  10049  canthp1lem2  10064  hashfacen  13808  hashf1lem1  13809  fprodss  15294  phimullem  16106  unbenlem  16234  0ram  16346  symgfixelsi  18555  symgfixf1  18557  f1omvdmvd  18563  f1omvdcnv  18564  f1omvdconj  18566  f1otrspeq  18567  symggen  18590  psgnunilem1  18613  dprdf1o  19147  znleval  20246  znunithash  20256  mdetdiaglem  21203  basqtop  22316  tgqtop  22317  reghmph  22398  ordthmeolem  22406  qtophmeo  22422  imasf1oxmet  22982  imasf1omet  22983  imasf1obl  23095  imasf1oxms  23096  cnheiborlem  23559  ovolctb  24094  mbfimaopnlem  24259  logblog  25378  axcontlem5  26762  nvinvfval  28423  adjbd1o  29868  isoun  30461  fsumiunle  30571  symgcom  30777  pmtrcnel  30783  psgnfzto1stlem  30792  tocycfvres1  30802  tocycfvres2  30803  cycpmfvlem  30804  cycpmfv3  30807  cycpmconjvlem  30833  cycpmrn  30835  cycpmconjslem2  30847  indf1ofs  31395  esumiun  31463  eulerpartgbij  31740  eulerpartlemgh  31746  ballotlemsima  31883  derangenlem  32531  subfacp1lem3  32542  subfacp1lem4  32543  subfacp1lem5  32544  fv1stcnv  33133  fv2ndcnv  33134  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem9  35066  poimirlem13  35070  poimirlem14  35071  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem23  35080  ltrnid  37431  ltrneq2  37444  cdleme51finvN  37852  diaintclN  38354  dibintclN  38463  mapdcl  38949  kelac1  40007  gicabl  40043  brco2f1o  40735  brco3f1o  40736  ntrclsfv1  40758  ntrneifv1  40782  clsneikex  40809  clsneinex  40810  neicvgmex  40820  neicvgel1  40822  stoweidlem27  42669  isomushgr  44344  isomuspgrlem1  44345  isomuspgrlem2b  44347  isomuspgrlem2d  44349  isomuspgr  44352  isomgrtrlem  44356