Theorem f1ofn 6819

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

Syntax hints:   → wi 4   Fn wfn 6526  –1-1-onto→wf1o 6530

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 207  df-an 396  df-f 6535  df-f1 6536  df-f1o 6538

This theorem is referenced by:  f1ofun  6820  f1odm  6822  fveqf1o  7295  f1ofvswap  7299  isomin  7330  isoini  7331  isofrlem  7333  isoselem  7334  weniso  7347  bren  8969  enfixsn  9095  dif1enlem  9170  dif1enlemOLD  9171  f1oenfi  9193  f1oenfirn  9194  f1domfi  9195  phplem2  9219  php3  9223  php3OLD  9233  domunfican  9333  fiint  9338  fiintOLD  9339  supisolem  9486  ordiso2  9529  unxpwdom2  9602  wemapwe  9711  djuun  9940  infxpenlem  10027  ackbij2lem2  10253  ackbij2lem3  10254  fpwwe2lem8  10652  canthp1lem2  10667  hashfacen  14472  hashf1lem1  14473  fprodss  15964  phimullem  16798  unbenlem  16928  0ram  17040  symgfixelsi  19416  symgfixf1  19418  f1omvdmvd  19424  f1omvdcnv  19425  f1omvdconj  19427  f1otrspeq  19428  symggen  19451  psgnunilem1  19474  dprdf1o  20015  znleval  21515  znunithash  21525  mdetdiaglem  22536  basqtop  23649  tgqtop  23650  reghmph  23731  ordthmeolem  23739  qtophmeo  23755  imasf1oxmet  24314  imasf1omet  24315  imasf1obl  24427  imasf1oxms  24428  cnheiborlem  24904  ovolctb  25443  mbfimaopnlem  25608  logblog  26754  axcontlem5  28947  nvinvfval  30621  adjbd1o  32066  isoun  32679  fsumiunle  32808  indf1ofs  32843  symgcom  33094  pmtrcnel  33100  psgnfzto1stlem  33111  tocycfvres1  33121  tocycfvres2  33122  cycpmfvlem  33123  cycpmfv3  33126  cycpmconjvlem  33152  cycpmrn  33154  cycpmconjslem2  33166  1arithidomlem2  33551  esumiun  34125  eulerpartgbij  34404  eulerpartlemgh  34410  ballotlemsima  34548  derangenlem  35193  subfacp1lem3  35204  subfacp1lem4  35205  subfacp1lem5  35206  fv1stcnv  35794  fv2ndcnv  35795  poimirlem1  37645  poimirlem2  37646  poimirlem3  37647  poimirlem4  37648  poimirlem6  37650  poimirlem7  37651  poimirlem8  37652  poimirlem9  37653  poimirlem13  37657  poimirlem14  37658  poimirlem15  37659  poimirlem16  37660  poimirlem17  37661  poimirlem19  37663  poimirlem20  37664  poimirlem23  37667  ltrnid  40154  ltrneq2  40167  cdleme51finvN  40575  diaintclN  41077  dibintclN  41186  mapdcl  41672  kelac1  43087  gicabl  43123  brco2f1o  44056  brco3f1o  44057  ntrclsfv1  44079  ntrneifv1  44103  clsneikex  44130  clsneinex  44131  neicvgmex  44141  neicvgel1  44143  brpermmodel  45028  permaxpow  45034  permaxun  45036  stoweidlem27  46056  3f1oss1  47104  uhgrimprop  47905  isuspgrimlem  47908  upgrimwlklem5  47914  gricushgr  47930  uhgrimisgrgric  47944  clnbgrgrimlem  47946  clnbgrgrim  47947  grtriclwlk3  47957  grimgrtri  47961  isubgr3stgrlem4  47981  isubgr3stgrlem7  47984  grlimgrtrilem2  48007