Theorem f1ofn 6850

Description: A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1ofn	⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹 Fn 𝐴)

Proof of Theorem f1ofn

Step	Hyp	Ref	Expression
1		f1of 6849	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹:𝐴⟶𝐵)
2	1	ffnd 6735	1 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹 Fn 𝐴)

This proof depends on syntax axioms:   → wi 4   Fn wfn 6556  ⟶1-1ontowf1o 6560

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 6565  df-f1 6566  df-f1o 6568

This theorem is used by:  f1ofun  6851  f1odm  6853  f1odmOLD  6854  fveqf1o  7336  f1ofvswap  7340  isomin  7371  isoini  7372  isofrlem  7374  isoselem  7375  weniso  7390  bren  9014  enfixsn  9136  dif1enlem  9206  f1oenfi  9225  f1oenfirn  9226  f1domfi  9227  phplem2  9251  php3  9255  domunfican  9344  fiint  9349  supisolem  9496  ordiso2  9539  unxpwdom2  9612  wemapwe  9728  djuun  10037  infxpenlem  10122  ackbij2lem2  10347  ackbij2lem3  10348  fpwwe2lem8  10753  canthp1lem2  10768  hashfacen  14629  hashf1lem1  14630  fprodss  16147  phimullem  16988  unbenlem  17118  0ram  17230  symgfixelsi  19682  symgfixf1  19684  f1omvdmvd  19690  f1omvdcnv  19691  f1omvdconj  19693  f1otrspeq  19694  symggen  19717  psgnunilem1  19740  dprdf1o  20281  znleval  21893  znunithash  21903  mdetdiaglem  22946  basqtop  24063  tgqtop  24064  reghmph  24145  ordthmeolem  24153  qtophmeo  24169  imasf1oxmet  24727  imasf1omet  24728  imasf1obl  24840  imasf1oxms  24841  cnheiborlem  25308  ovolctb  25844  mbfimaopnlem  26009  logblog  27153  axcontlem5  29579  nvinvfval  31275  adjbd1o  32720  isoun  33369  fsumiunle  33493  indf1ofs  33506  symgcom  33720  pmtrcnel  33726  psgnfzto1stlem  33737  tocycfvres1  33747  tocycfvres2  33748  cycpmfvlem  33749  cycpmfv3  33752  cycpmconjvlem  33778  cycpmrn  33780  cycpmconjslem2  33792  1arithidomlem2  34152  esumiun  34809  eulerpartgbij  35087  eulerpartlemgh  35093  ballotlemsima  35231  vonf1owevOLD  36051  prconf1acwevd  36061  onprcf1of1ord  36068  derangenlem  36116  subfacp1lem3  36127  subfacp1lem4  36128  subfacp1lem5  36129  fv1stcnv  36732  fv2ndcnv  36733  poimirlem1  38744  poimirlem2  38745  poimirlem3  38746  poimirlem4  38747  poimirlem6  38749  poimirlem7  38750  poimirlem8  38751  poimirlem9  38752  poimirlem13  38756  poimirlem14  38757  poimirlem15  38758  poimirlem16  38759  poimirlem17  38760  poimirlem19  38762  poimirlem20  38763  poimirlem23  38766  ltrnid  41395  ltrneq2  41408  cdleme51finvN  41816  diaintclN  42318  dibintclN  42427  mapdcl  42913  kelac1  44269  gicabl  44305  brco2f1o  45235  brco3f1o  45236  ntrclsfv1  45258  ntrneifv1  45282  clsneikex  45309  clsneinex  45310  neicvgmex  45320  neicvgel1  45322  brpermmodel  46199  permaxpow  46205  permaxun  46207  permac8prim  46210  stoweidlem27  47252  3f1oss1  48360  uhgrimprop  49205  isuspgrimlem  49208  upgrimwlklem5  49214  gricushgr  49230  uhgrimisgrgric  49244  clnbgrgrimlem  49246  clnbgrgrim  49247  grtriclwlk3  49258  grimgrtri  49262  isubgr3stgrlem4  49282  isubgr3stgrlem7  49285  grlimprclnbgr  49309  grlimgrtrilem2  49315