Theorem f1ofn 6822

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6532  –1-1-onto→wf1o 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6541  df-f1 6542  df-f1o 6544

This theorem is used by:  f1ofun  6823  f1odm  6825  f1odmOLD  6826  fveqf1o  7307  f1ofvswap  7311  isomin  7342  isoini  7343  isofrlem  7345  isoselem  7346  weniso  7361  bren  8966  enfixsn  9088  dif1enlem  9158  f1oenfi  9177  f1oenfirn  9178  f1domfi  9179  phplem2  9203  php3  9207  domunfican  9295  fiint  9300  supisolem  9448  ordiso2  9491  unxpwdom2  9564  wemapwe  9680  djuun  9935  infxpenlem  10020  ackbij2lem2  10245  ackbij2lem3  10246  fpwwe2lem8  10651  canthp1lem2  10666  hashfacen  14523  hashf1lem1  14524  fprodss  16041  phimullem  16876  unbenlem  17006  0ram  17118  symgfixelsi  19568  symgfixf1  19570  f1omvdmvd  19576  f1omvdcnv  19577  f1omvdconj  19579  f1otrspeq  19580  symggen  19603  psgnunilem1  19626  dprdf1o  20167  znleval  21773  znunithash  21783  mdetdiaglem  22826  basqtop  23943  tgqtop  23944  reghmph  24025  ordthmeolem  24033  qtophmeo  24049  imasf1oxmet  24607  imasf1omet  24608  imasf1obl  24720  imasf1oxms  24721  cnheiborlem  25188  ovolctb  25724  mbfimaopnlem  25889  logblog  27037  axcontlem5  29433  nvinvfval  31129  adjbd1o  32574  isoun  33182  fsumiunle  33307  indf1ofs  33320  symgcom  33531  pmtrcnel  33537  psgnfzto1stlem  33548  tocycfvres1  33558  tocycfvres2  33559  cycpmfvlem  33560  cycpmfv3  33563  cycpmconjvlem  33589  cycpmrn  33591  cycpmconjslem2  33603  1arithidomlem2  33954  esumiun  34612  eulerpartgbij  34891  eulerpartlemgh  34897  ballotlemsima  35035  vonf1owevOLD  35715  derangenlem  35758  subfacp1lem3  35769  subfacp1lem4  35770  subfacp1lem5  35771  fv1stcnv  36364  fv2ndcnv  36365  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem9  38386  poimirlem13  38390  poimirlem14  38391  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem23  38400  ltrnid  41016  ltrneq2  41029  cdleme51finvN  41437  diaintclN  41939  dibintclN  42048  mapdcl  42534  kelac1  43912  gicabl  43948  brco2f1o  44880  brco3f1o  44881  ntrclsfv1  44903  ntrneifv1  44927  clsneikex  44954  clsneinex  44955  neicvgmex  44965  neicvgel1  44967  brpermmodel  45834  permaxpow  45840  permaxun  45842  permac8prim  45845  stoweidlem27  46863  3f1oss1  47971  uhgrimprop  48816  isuspgrimlem  48819  upgrimwlklem5  48825  gricushgr  48841  uhgrimisgrgric  48855  clnbgrgrimlem  48857  clnbgrgrim  48858  grtriclwlk3  48869  grimgrtri  48873  isubgr3stgrlem4  48893  isubgr3stgrlem7  48896  grlimprclnbgr  48920  grlimgrtrilem2  48926