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 6556  –1-1-onto→wf1o 6560

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

This theorem is referenced by:  f1ofun  6850  f1odm  6852  fveqf1o  7322  f1ofvswap  7326  isomin  7357  isoini  7358  isofrlem  7360  isoselem  7361  weniso  7374  bren  8995  enfixsn  9121  dif1enlem  9196  dif1enlemOLD  9197  f1oenfi  9219  f1oenfirn  9220  f1domfi  9221  phplem2  9245  php3  9249  phplem4OLD  9257  php3OLD  9261  domunfican  9361  fiint  9366  fiintOLD  9367  supisolem  9513  ordiso2  9555  unxpwdom2  9628  wemapwe  9737  djuun  9966  infxpenlem  10053  ackbij2lem2  10279  ackbij2lem3  10280  fpwwe2lem8  10678  canthp1lem2  10693  hashfacen  14493  hashf1lem1  14494  fprodss  15984  phimullem  16816  unbenlem  16946  0ram  17058  symgfixelsi  19453  symgfixf1  19455  f1omvdmvd  19461  f1omvdcnv  19462  f1omvdconj  19464  f1otrspeq  19465  symggen  19488  psgnunilem1  19511  dprdf1o  20052  znleval  21573  znunithash  21583  mdetdiaglem  22604  basqtop  23719  tgqtop  23720  reghmph  23801  ordthmeolem  23809  qtophmeo  23825  imasf1oxmet  24385  imasf1omet  24386  imasf1obl  24501  imasf1oxms  24502  cnheiborlem  24986  ovolctb  25525  mbfimaopnlem  25690  logblog  26835  axcontlem5  28983  nvinvfval  30659  adjbd1o  32104  isoun  32711  fsumiunle  32831  indf1ofs  32851  symgcom  33103  pmtrcnel  33109  psgnfzto1stlem  33120  tocycfvres1  33130  tocycfvres2  33131  cycpmfvlem  33132  cycpmfv3  33135  cycpmconjvlem  33161  cycpmrn  33163  cycpmconjslem2  33175  1arithidomlem2  33564  esumiun  34095  eulerpartgbij  34374  eulerpartlemgh  34380  ballotlemsima  34518  derangenlem  35176  subfacp1lem3  35187  subfacp1lem4  35188  subfacp1lem5  35189  fv1stcnv  35777  fv2ndcnv  35778  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem9  37636  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem23  37650  ltrnid  40137  ltrneq2  40150  cdleme51finvN  40558  diaintclN  41060  dibintclN  41169  mapdcl  41655  kelac1  43075  gicabl  43111  brco2f1o  44045  brco3f1o  44046  ntrclsfv1  44068  ntrneifv1  44092  clsneikex  44119  clsneinex  44120  neicvgmex  44130  neicvgel1  44132  stoweidlem27  46042  3f1oss1  47087  uspgrimprop  47873  isuspgrimlem  47874  gricushgr  47886  uhgrimisgrgric  47899  clnbgrgrimlem  47901  clnbgrgrim  47902  grtriclwlk3  47912  grimgrtri  47916  isubgr3stgrlem4  47936  isubgr3stgrlem7  47939  grlimgrtrilem2  47962