Theorem f1ofn 6764

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

Syntax hints:   → wi 4   Fn wfn 6476  –1-1-onto→wf1o 6480

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 6485  df-f1 6486  df-f1o 6488

This theorem is referenced by:  f1ofun  6765  f1odm  6767  fveqf1o  7236  f1ofvswap  7240  isomin  7271  isoini  7272  isofrlem  7274  isoselem  7275  weniso  7288  bren  8879  enfixsn  8999  dif1enlem  9069  f1oenfi  9088  f1oenfirn  9089  f1domfi  9090  phplem2  9114  php3  9118  domunfican  9206  fiint  9211  supisolem  9358  ordiso2  9401  unxpwdom2  9474  wemapwe  9587  djuun  9819  infxpenlem  9904  ackbij2lem2  10130  ackbij2lem3  10131  fpwwe2lem8  10529  canthp1lem2  10544  hashfacen  14361  hashf1lem1  14362  fprodss  15855  phimullem  16690  unbenlem  16820  0ram  16932  symgfixelsi  19348  symgfixf1  19350  f1omvdmvd  19356  f1omvdcnv  19357  f1omvdconj  19359  f1otrspeq  19360  symggen  19383  psgnunilem1  19406  dprdf1o  19947  znleval  21492  znunithash  21502  mdetdiaglem  22514  basqtop  23627  tgqtop  23628  reghmph  23709  ordthmeolem  23717  qtophmeo  23733  imasf1oxmet  24291  imasf1omet  24292  imasf1obl  24404  imasf1oxms  24405  cnheiborlem  24881  ovolctb  25419  mbfimaopnlem  25584  logblog  26730  axcontlem5  28947  nvinvfval  30618  adjbd1o  32063  isoun  32681  fsumiunle  32810  indf1ofs  32845  symgcom  33050  pmtrcnel  33056  psgnfzto1stlem  33067  tocycfvres1  33077  tocycfvres2  33078  cycpmfvlem  33079  cycpmfv3  33082  cycpmconjvlem  33108  cycpmrn  33110  cycpmconjslem2  33122  1arithidomlem2  33499  esumiun  34105  eulerpartgbij  34383  eulerpartlemgh  34389  ballotlemsima  34527  vonf1owev  35150  derangenlem  35213  subfacp1lem3  35224  subfacp1lem4  35225  subfacp1lem5  35226  fv1stcnv  35819  fv2ndcnv  35820  poimirlem1  37667  poimirlem2  37668  poimirlem3  37669  poimirlem4  37670  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem9  37675  poimirlem13  37679  poimirlem14  37680  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  poimirlem23  37689  ltrnid  40180  ltrneq2  40193  cdleme51finvN  40601  diaintclN  41103  dibintclN  41212  mapdcl  41698  kelac1  43102  gicabl  43138  brco2f1o  44071  brco3f1o  44072  ntrclsfv1  44094  ntrneifv1  44118  clsneikex  44145  clsneinex  44146  neicvgmex  44156  neicvgel1  44158  brpermmodel  45042  permaxpow  45048  permaxun  45050  permac8prim  45053  stoweidlem27  46071  3f1oss1  47112  uhgrimprop  47929  isuspgrimlem  47932  upgrimwlklem5  47938  gricushgr  47954  uhgrimisgrgric  47968  clnbgrgrimlem  47970  clnbgrgrim  47971  grtriclwlk3  47982  grimgrtri  47986  isubgr3stgrlem4  48006  isubgr3stgrlem7  48009  grlimprclnbgr  48033  grlimgrtrilem2  48039