Theorem f1ofn 6826

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6534  –1-1-onto→wf1o 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6543  df-f1 6544  df-f1o 6546

This theorem is used by:  f1ofun  6827  f1odm  6829  f1odmOLD  6830  fveqf1o  7311  f1ofvswap  7315  isomin  7346  isoini  7347  isofrlem  7349  isoselem  7350  weniso  7365  bren  8987  enfixsn  9109  dif1enlem  9179  f1oenfi  9198  f1oenfirn  9199  f1domfi  9200  phplem2  9224  php3  9228  domunfican  9317  fiint  9322  supisolem  9470  ordiso2  9513  unxpwdom2  9586  wemapwe  9702  djuun  10011  infxpenlem  10096  ackbij2lem2  10321  ackbij2lem3  10322  fpwwe2lem8  10727  canthp1lem2  10742  hashfacen  14603  hashf1lem1  14604  fprodss  16121  phimullem  16962  unbenlem  17092  0ram  17204  symgfixelsi  19655  symgfixf1  19657  f1omvdmvd  19663  f1omvdcnv  19664  f1omvdconj  19666  f1otrspeq  19667  symggen  19690  psgnunilem1  19713  dprdf1o  20254  znleval  21866  znunithash  21876  mdetdiaglem  22919  basqtop  24036  tgqtop  24037  reghmph  24118  ordthmeolem  24126  qtophmeo  24142  imasf1oxmet  24700  imasf1omet  24701  imasf1obl  24813  imasf1oxms  24814  cnheiborlem  25281  ovolctb  25817  mbfimaopnlem  25982  logblog  27126  axcontlem5  29552  nvinvfval  31248  adjbd1o  32693  isoun  33343  fsumiunle  33467  indf1ofs  33480  symgcom  33691  pmtrcnel  33697  psgnfzto1stlem  33708  tocycfvres1  33718  tocycfvres2  33719  cycpmfvlem  33720  cycpmfv3  33723  cycpmconjvlem  33749  cycpmrn  33751  cycpmconjslem2  33763  1arithidomlem2  34115  esumiun  34773  eulerpartgbij  35051  eulerpartlemgh  35057  ballotlemsima  35195  vonf1owevOLD  35958  prconf1acwevd  35968  onprcf1of1ord  35975  derangenlem  36023  subfacp1lem3  36034  subfacp1lem4  36035  subfacp1lem5  36036  fv1stcnv  36634  fv2ndcnv  36635  poimirlem1  38633  poimirlem2  38634  poimirlem3  38635  poimirlem4  38636  poimirlem6  38638  poimirlem7  38639  poimirlem8  38640  poimirlem9  38641  poimirlem13  38645  poimirlem14  38646  poimirlem15  38647  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem23  38655  ltrnid  41286  ltrneq2  41299  cdleme51finvN  41707  diaintclN  42209  dibintclN  42318  mapdcl  42804  kelac1  44159  gicabl  44195  brco2f1o  45126  brco3f1o  45127  ntrclsfv1  45149  ntrneifv1  45173  clsneikex  45200  clsneinex  45201  neicvgmex  45211  neicvgel1  45213  brpermmodel  46087  permaxpow  46093  permaxun  46095  permac8prim  46098  stoweidlem27  47131  3f1oss1  48239  uhgrimprop  49084  isuspgrimlem  49087  upgrimwlklem5  49093  gricushgr  49109  uhgrimisgrgric  49123  clnbgrgrimlem  49125  clnbgrgrim  49126  grtriclwlk3  49137  grimgrtri  49141  isubgr3stgrlem4  49161  isubgr3stgrlem7  49164  grlimprclnbgr  49188  grlimgrtrilem2  49194