Theorem f1ofn 6051

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 6050	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
2		ffn 5958	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5799  ⟶wf 5800  –1-1-onto→wf1o 5803

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 196  df-an 385  df-f 5808  df-f1 5809  df-f1o 5811

This theorem is referenced by:  f1ofun  6052  f1odm  6054  fveqf1o  6457  isomin  6487  isoini  6488  isofrlem  6490  isoselem  6491  weniso  6504  bren  7850  enfixsn  7954  phplem4  8027  php3  8031  domunfican  8118  fiint  8122  supisolem  8262  ordiso2  8303  unxpwdom2  8376  wemapwe  8477  infxpenlem  8719  ackbij2lem2  8945  ackbij2lem3  8946  fpwwe2lem9  9339  canthp1lem2  9354  hashfacen  13095  hashf1lem1  13096  fprodss  14517  phimullem  15322  unbenlem  15450  0ram  15562  symgfixelsi  17678  symgfixf1  17680  f1omvdmvd  17686  f1omvdcnv  17687  f1omvdconj  17689  f1otrspeq  17690  symggen  17713  psgnunilem1  17736  dprdf1o  18254  znleval  19722  znunithash  19732  mdetdiaglem  20223  basqtop  21324  tgqtop  21325  reghmph  21406  ordthmeolem  21414  qtophmeo  21430  imasf1oxmet  21990  imasf1omet  21991  imasf1obl  22103  imasf1oxms  22104  cnheiborlem  22561  ovolctb  23065  mbfimaopnlem  23228  logblog  24330  axcontlem5  25648  vdgr1d  26430  vdgr1b  26431  vdgr1a  26433  eupai  26494  eupatrl  26495  eupap1  26503  eupath2lem3  26506  vdegp1ai  26511  vdegp1bi  26512  nvinvfval  26879  adjbd1o  28328  isoun  28862  psgnfzto1stlem  29181  indf1ofs  29415  esumiun  29483  eulerpartgbij  29761  eulerpartlemgh  29767  ballotlemsima  29904  derangenlem  30407  subfacp1lem3  30418  subfacp1lem4  30419  subfacp1lem5  30420  fv1stcnv  30925  fv2ndcnv  30926  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem9  32588  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem23  32602  ltrnid  34439  ltrneq2  34452  cdleme51finvN  34862  diaintclN  35365  dibintclN  35474  mapdcl  35960  kelac1  36651  gicabl  36687  brco2f1o  37350  brco3f1o  37351  ntrclsfv1  37373  ntrneifv1  37397  clsneikex  37424  clsneinex  37425  neicvgmex  37435  neicvgel1  37437  stoweidlem27  38920