Theorem f1ofn 6863

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

Syntax hints:   → wi 4   Fn wfn 6568  –1-1-onto→wf1o 6572

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 6577  df-f1 6578  df-f1o 6580

This theorem is referenced by:  f1ofun  6864  f1odm  6866  fveqf1o  7338  f1ofvswap  7342  isomin  7373  isoini  7374  isofrlem  7376  isoselem  7377  weniso  7390  bren  9013  brenOLD  9014  enfixsn  9147  dif1enlem  9222  dif1enlemOLD  9223  f1oenfi  9245  f1oenfirn  9246  f1domfi  9247  phplem2  9271  php3  9275  phplem4OLD  9283  php3OLD  9287  domunfican  9389  fiint  9394  fiintOLD  9395  supisolem  9542  ordiso2  9584  unxpwdom2  9657  wemapwe  9766  djuun  9995  infxpenlem  10082  ackbij2lem2  10308  ackbij2lem3  10309  fpwwe2lem8  10707  canthp1lem2  10722  hashfacen  14503  hashf1lem1  14504  fprodss  15996  phimullem  16826  unbenlem  16955  0ram  17067  symgfixelsi  19477  symgfixf1  19479  f1omvdmvd  19485  f1omvdcnv  19486  f1omvdconj  19488  f1otrspeq  19489  symggen  19512  psgnunilem1  19535  dprdf1o  20076  znleval  21596  znunithash  21606  mdetdiaglem  22625  basqtop  23740  tgqtop  23741  reghmph  23822  ordthmeolem  23830  qtophmeo  23846  imasf1oxmet  24406  imasf1omet  24407  imasf1obl  24522  imasf1oxms  24523  cnheiborlem  25005  ovolctb  25544  mbfimaopnlem  25709  logblog  26853  axcontlem5  29001  nvinvfval  30672  adjbd1o  32117  isoun  32713  fsumiunle  32833  symgcom  33076  pmtrcnel  33082  psgnfzto1stlem  33093  tocycfvres1  33103  tocycfvres2  33104  cycpmfvlem  33105  cycpmfv3  33108  cycpmconjvlem  33134  cycpmrn  33136  cycpmconjslem2  33148  1arithidomlem2  33529  indf1ofs  33990  esumiun  34058  eulerpartgbij  34337  eulerpartlemgh  34343  ballotlemsima  34480  derangenlem  35139  subfacp1lem3  35150  subfacp1lem4  35151  subfacp1lem5  35152  fv1stcnv  35740  fv2ndcnv  35741  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem9  37589  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  ltrnid  40092  ltrneq2  40105  cdleme51finvN  40513  diaintclN  41015  dibintclN  41124  mapdcl  41610  kelac1  43020  gicabl  43056  brco2f1o  43994  brco3f1o  43995  ntrclsfv1  44017  ntrneifv1  44041  clsneikex  44068  clsneinex  44069  neicvgmex  44079  neicvgel1  44081  stoweidlem27  45948  3f1oss1  46990  uspgrimprop  47757  isuspgrimlem  47758  gricushgr  47770  uhgrimisgrgric  47783  clnbgrgrimlem  47785  clnbgrgrim  47786  grtriclwlk3  47796  grimgrtri  47798  grlimgrtrilem2  47819