Theorem f1ofn 6138

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

Syntax hints:   → wi 4   Fn wfn 5883  ⟶wf 5884  –1-1-onto→wf1o 5887

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 197  df-an 386  df-f 5892  df-f1 5893  df-f1o 5895

This theorem is referenced by:  f1ofun  6139  f1odm  6141  fveqf1o  6557  isomin  6587  isoini  6588  isofrlem  6590  isoselem  6591  weniso  6604  bren  7964  enfixsn  8069  phplem4  8142  php3  8146  domunfican  8233  fiint  8237  supisolem  8379  ordiso2  8420  unxpwdom2  8493  wemapwe  8594  infxpenlem  8836  ackbij2lem2  9062  ackbij2lem3  9063  fpwwe2lem9  9460  canthp1lem2  9475  hashfacen  13238  hashf1lem1  13239  fprodss  14678  phimullem  15484  unbenlem  15612  0ram  15724  symgfixelsi  17855  symgfixf1  17857  f1omvdmvd  17863  f1omvdcnv  17864  f1omvdconj  17866  f1otrspeq  17867  symggen  17890  psgnunilem1  17913  dprdf1o  18431  znleval  19903  znunithash  19913  mdetdiaglem  20404  basqtop  21514  tgqtop  21515  reghmph  21596  ordthmeolem  21604  qtophmeo  21620  imasf1oxmet  22180  imasf1omet  22181  imasf1obl  22293  imasf1oxms  22294  cnheiborlem  22753  ovolctb  23258  mbfimaopnlem  23422  logblog  24530  axcontlem5  25848  nvinvfval  27495  adjbd1o  28944  isoun  29479  fsumiunle  29575  psgnfzto1stlem  29850  indf1ofs  30088  esumiun  30156  eulerpartgbij  30434  eulerpartlemgh  30440  ballotlemsima  30577  derangenlem  31153  subfacp1lem3  31164  subfacp1lem4  31165  subfacp1lem5  31166  fv1stcnv  31680  fv2ndcnv  31681  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem23  33432  ltrnid  35421  ltrneq2  35434  cdleme51finvN  35844  diaintclN  36347  dibintclN  36456  mapdcl  36942  kelac1  37633  gicabl  37669  brco2f1o  38330  brco3f1o  38331  ntrclsfv1  38353  ntrneifv1  38377  clsneikex  38404  clsneinex  38405  neicvgmex  38415  neicvgel1  38417  stoweidlem27  40244