Theorem f1ofn 6834

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

Syntax hints:   → wi 4   Fn wfn 6538  –1-1-onto→wf1o 6542

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 206  df-an 397  df-f 6547  df-f1 6548  df-f1o 6550

This theorem is referenced by:  f1ofun  6835  f1odm  6837  fveqf1o  7303  f1ofvswap  7306  isomin  7336  isoini  7337  isofrlem  7339  isoselem  7340  weniso  7353  bren  8951  brenOLD  8952  enfixsn  9083  dif1enlem  9158  dif1enlemOLD  9159  f1oenfi  9184  f1oenfirn  9185  f1domfi  9186  phplem2  9210  php3  9214  phplem4OLD  9222  php3OLD  9226  domunfican  9322  fiint  9326  supisolem  9470  ordiso2  9512  unxpwdom2  9585  wemapwe  9694  djuun  9923  infxpenlem  10010  ackbij2lem2  10237  ackbij2lem3  10238  fpwwe2lem8  10635  canthp1lem2  10650  hashfacen  14417  hashfacenOLD  14418  hashf1lem1  14419  hashf1lem1OLD  14420  fprodss  15896  phimullem  16716  unbenlem  16845  0ram  16957  symgfixelsi  19344  symgfixf1  19346  f1omvdmvd  19352  f1omvdcnv  19353  f1omvdconj  19355  f1otrspeq  19356  symggen  19379  psgnunilem1  19402  dprdf1o  19943  znleval  21329  znunithash  21339  mdetdiaglem  22320  basqtop  23435  tgqtop  23436  reghmph  23517  ordthmeolem  23525  qtophmeo  23541  imasf1oxmet  24101  imasf1omet  24102  imasf1obl  24217  imasf1oxms  24218  cnheiborlem  24694  ovolctb  25231  mbfimaopnlem  25396  logblog  26521  axcontlem5  28481  nvinvfval  30148  adjbd1o  31593  isoun  32178  fsumiunle  32290  symgcom  32502  pmtrcnel  32508  psgnfzto1stlem  32517  tocycfvres1  32527  tocycfvres2  32528  cycpmfvlem  32529  cycpmfv3  32532  cycpmconjvlem  32558  cycpmrn  32560  cycpmconjslem2  32572  indf1ofs  33310  esumiun  33378  eulerpartgbij  33657  eulerpartlemgh  33663  ballotlemsima  33800  derangenlem  34448  subfacp1lem3  34459  subfacp1lem4  34460  subfacp1lem5  34461  fv1stcnv  35040  fv2ndcnv  35041  poimirlem1  36792  poimirlem2  36793  poimirlem3  36794  poimirlem4  36795  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  poimirlem9  36800  poimirlem13  36804  poimirlem14  36805  poimirlem15  36806  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem23  36814  ltrnid  39309  ltrneq2  39322  cdleme51finvN  39730  diaintclN  40232  dibintclN  40341  mapdcl  40827  kelac1  42107  gicabl  42143  brco2f1o  43085  brco3f1o  43086  ntrclsfv1  43108  ntrneifv1  43132  clsneikex  43159  clsneinex  43160  neicvgmex  43170  neicvgel1  43172  stoweidlem27  45042  isomushgr  46793  isomuspgrlem1  46794  isomuspgrlem2b  46796  isomuspgrlem2d  46798  isomuspgr  46801  isomgrtrlem  46805