Theorem f1ofn 6801

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

Syntax hints:   → wi 4   Fn wfn 6506  –1-1-onto→wf1o 6510

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 6515  df-f1 6516  df-f1o 6518

This theorem is referenced by:  f1ofun  6802  f1odm  6804  fveqf1o  7277  f1ofvswap  7281  isomin  7312  isoini  7313  isofrlem  7315  isoselem  7316  weniso  7329  bren  8928  enfixsn  9050  dif1enlem  9120  dif1enlemOLD  9121  f1oenfi  9143  f1oenfirn  9144  f1domfi  9145  phplem2  9169  php3  9173  domunfican  9272  fiint  9277  fiintOLD  9278  supisolem  9425  ordiso2  9468  unxpwdom2  9541  wemapwe  9650  djuun  9879  infxpenlem  9966  ackbij2lem2  10192  ackbij2lem3  10193  fpwwe2lem8  10591  canthp1lem2  10606  hashfacen  14419  hashf1lem1  14420  fprodss  15914  phimullem  16749  unbenlem  16879  0ram  16991  symgfixelsi  19365  symgfixf1  19367  f1omvdmvd  19373  f1omvdcnv  19374  f1omvdconj  19376  f1otrspeq  19377  symggen  19400  psgnunilem1  19423  dprdf1o  19964  znleval  21464  znunithash  21474  mdetdiaglem  22485  basqtop  23598  tgqtop  23599  reghmph  23680  ordthmeolem  23688  qtophmeo  23704  imasf1oxmet  24263  imasf1omet  24264  imasf1obl  24376  imasf1oxms  24377  cnheiborlem  24853  ovolctb  25391  mbfimaopnlem  25556  logblog  26702  axcontlem5  28895  nvinvfval  30569  adjbd1o  32014  isoun  32625  fsumiunle  32754  indf1ofs  32789  symgcom  33040  pmtrcnel  33046  psgnfzto1stlem  33057  tocycfvres1  33067  tocycfvres2  33068  cycpmfvlem  33069  cycpmfv3  33072  cycpmconjvlem  33098  cycpmrn  33100  cycpmconjslem2  33112  1arithidomlem2  33507  esumiun  34084  eulerpartgbij  34363  eulerpartlemgh  34369  ballotlemsima  34507  vonf1owev  35095  derangenlem  35158  subfacp1lem3  35169  subfacp1lem4  35170  subfacp1lem5  35171  fv1stcnv  35764  fv2ndcnv  35765  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem9  37623  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  ltrnid  40129  ltrneq2  40142  cdleme51finvN  40550  diaintclN  41052  dibintclN  41161  mapdcl  41647  kelac1  43052  gicabl  43088  brco2f1o  44021  brco3f1o  44022  ntrclsfv1  44044  ntrneifv1  44068  clsneikex  44095  clsneinex  44096  neicvgmex  44106  neicvgel1  44108  brpermmodel  44993  permaxpow  44999  permaxun  45001  permac8prim  45004  stoweidlem27  46025  3f1oss1  47076  uhgrimprop  47892  isuspgrimlem  47895  upgrimwlklem5  47901  gricushgr  47917  uhgrimisgrgric  47931  clnbgrgrimlem  47933  clnbgrgrim  47934  grtriclwlk3  47944  grimgrtri  47948  isubgr3stgrlem4  47968  isubgr3stgrlem7  47971  grlimgrtrilem2  47994