Theorem f1ofn 6781

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

Syntax hints:   → wi 4   Fn wfn 6493  –1-1-onto→wf1o 6497

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 6502  df-f1 6503  df-f1o 6505

This theorem is referenced by:  f1ofun  6782  f1odm  6784  fveqf1o  7257  f1ofvswap  7261  isomin  7292  isoini  7293  isofrlem  7295  isoselem  7296  weniso  7309  bren  8903  enfixsn  9024  dif1enlem  9094  f1oenfi  9113  f1oenfirn  9114  f1domfi  9115  phplem2  9139  php3  9143  domunfican  9232  fiint  9237  supisolem  9387  ordiso2  9430  unxpwdom2  9503  wemapwe  9618  djuun  9850  infxpenlem  9935  ackbij2lem2  10161  ackbij2lem3  10162  fpwwe2lem8  10561  canthp1lem2  10576  hashfacen  14416  hashf1lem1  14417  fprodss  15913  phimullem  16749  unbenlem  16879  0ram  16991  symgfixelsi  19410  symgfixf1  19412  f1omvdmvd  19418  f1omvdcnv  19419  f1omvdconj  19421  f1otrspeq  19422  symggen  19445  psgnunilem1  19468  dprdf1o  20009  znleval  21534  znunithash  21544  mdetdiaglem  22563  basqtop  23676  tgqtop  23677  reghmph  23758  ordthmeolem  23766  qtophmeo  23782  imasf1oxmet  24340  imasf1omet  24341  imasf1obl  24453  imasf1oxms  24454  cnheiborlem  24921  ovolctb  25457  mbfimaopnlem  25622  logblog  26756  axcontlem5  29037  nvinvfval  30711  adjbd1o  32156  isoun  32775  fsumiunle  32902  indf1ofs  32926  symgcom  33144  pmtrcnel  33150  psgnfzto1stlem  33161  tocycfvres1  33171  tocycfvres2  33172  cycpmfvlem  33173  cycpmfv3  33176  cycpmconjvlem  33202  cycpmrn  33204  cycpmconjslem2  33216  1arithidomlem2  33596  esumiun  34238  eulerpartgbij  34516  eulerpartlemgh  34522  ballotlemsima  34660  vonf1owev  35290  derangenlem  35353  subfacp1lem3  35364  subfacp1lem4  35365  subfacp1lem5  35366  fv1stcnv  35959  fv2ndcnv  35960  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem9  37950  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem23  37964  ltrnid  40581  ltrneq2  40594  cdleme51finvN  41002  diaintclN  41504  dibintclN  41613  mapdcl  42099  kelac1  43491  gicabl  43527  brco2f1o  44459  brco3f1o  44460  ntrclsfv1  44482  ntrneifv1  44506  clsneikex  44533  clsneinex  44534  neicvgmex  44544  neicvgel1  44546  brpermmodel  45430  permaxpow  45436  permaxun  45438  permac8prim  45441  stoweidlem27  46455  3f1oss1  47523  uhgrimprop  48368  isuspgrimlem  48371  upgrimwlklem5  48377  gricushgr  48393  uhgrimisgrgric  48407  clnbgrgrimlem  48409  clnbgrgrim  48410  grtriclwlk3  48421  grimgrtri  48425  isubgr3stgrlem4  48445  isubgr3stgrlem7  48448  grlimprclnbgr  48472  grlimgrtrilem2  48478