Theorem f1ofn 6849

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

Syntax hints:   → wi 4   Fn wfn 6557  –1-1-onto→wf1o 6561

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 6566  df-f1 6567  df-f1o 6569

This theorem is referenced by:  f1ofun  6850  f1odm  6852  fveqf1o  7321  f1ofvswap  7325  isomin  7356  isoini  7357  isofrlem  7359  isoselem  7360  weniso  7373  bren  8993  enfixsn  9119  dif1enlem  9194  dif1enlemOLD  9195  f1oenfi  9216  f1oenfirn  9217  f1domfi  9218  phplem2  9242  php3  9246  phplem4OLD  9254  php3OLD  9258  domunfican  9358  fiint  9363  fiintOLD  9364  supisolem  9510  ordiso2  9552  unxpwdom2  9625  wemapwe  9734  djuun  9963  infxpenlem  10050  ackbij2lem2  10276  ackbij2lem3  10277  fpwwe2lem8  10675  canthp1lem2  10690  hashfacen  14489  hashf1lem1  14490  fprodss  15980  phimullem  16812  unbenlem  16941  0ram  17053  symgfixelsi  19467  symgfixf1  19469  f1omvdmvd  19475  f1omvdcnv  19476  f1omvdconj  19478  f1otrspeq  19479  symggen  19502  psgnunilem1  19525  dprdf1o  20066  znleval  21590  znunithash  21600  mdetdiaglem  22619  basqtop  23734  tgqtop  23735  reghmph  23816  ordthmeolem  23824  qtophmeo  23840  imasf1oxmet  24400  imasf1omet  24401  imasf1obl  24516  imasf1oxms  24517  cnheiborlem  24999  ovolctb  25538  mbfimaopnlem  25703  logblog  26849  axcontlem5  28997  nvinvfval  30668  adjbd1o  32113  isoun  32716  fsumiunle  32835  symgcom  33085  pmtrcnel  33091  psgnfzto1stlem  33102  tocycfvres1  33112  tocycfvres2  33113  cycpmfvlem  33114  cycpmfv3  33117  cycpmconjvlem  33143  cycpmrn  33145  cycpmconjslem2  33157  1arithidomlem2  33543  indf1ofs  34006  esumiun  34074  eulerpartgbij  34353  eulerpartlemgh  34359  ballotlemsima  34496  derangenlem  35155  subfacp1lem3  35166  subfacp1lem4  35167  subfacp1lem5  35168  fv1stcnv  35757  fv2ndcnv  35758  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem9  37615  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem23  37629  ltrnid  40117  ltrneq2  40130  cdleme51finvN  40538  diaintclN  41040  dibintclN  41149  mapdcl  41635  kelac1  43051  gicabl  43087  brco2f1o  44021  brco3f1o  44022  ntrclsfv1  44044  ntrneifv1  44068  clsneikex  44095  clsneinex  44096  neicvgmex  44106  neicvgel1  44108  stoweidlem27  45982  3f1oss1  47024  uspgrimprop  47810  isuspgrimlem  47811  gricushgr  47823  uhgrimisgrgric  47836  clnbgrgrimlem  47838  clnbgrgrim  47839  grtriclwlk3  47849  grimgrtri  47851  isubgr3stgrlem4  47871  isubgr3stgrlem7  47874  grlimgrtrilem2  47897