Theorem f1ofn 6835

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

Syntax hints:   → wi 4   Fn wfn 6539  –1-1-onto→wf1o 6543

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 206  df-an 398  df-f 6548  df-f1 6549  df-f1o 6551

This theorem is referenced by:  f1ofun  6836  f1odm  6838  fveqf1o  7301  f1ofvswap  7304  isomin  7334  isoini  7335  isofrlem  7337  isoselem  7338  weniso  7351  bren  8949  brenOLD  8950  enfixsn  9081  dif1enlem  9156  dif1enlemOLD  9157  f1oenfi  9182  f1oenfirn  9183  f1domfi  9184  phplem2  9208  php3  9212  phplem4OLD  9220  php3OLD  9224  domunfican  9320  fiint  9324  supisolem  9468  ordiso2  9510  unxpwdom2  9583  wemapwe  9692  djuun  9921  infxpenlem  10008  ackbij2lem2  10235  ackbij2lem3  10236  fpwwe2lem8  10633  canthp1lem2  10648  hashfacen  14413  hashfacenOLD  14414  hashf1lem1  14415  hashf1lem1OLD  14416  fprodss  15892  phimullem  16712  unbenlem  16841  0ram  16953  symgfixelsi  19303  symgfixf1  19305  f1omvdmvd  19311  f1omvdcnv  19312  f1omvdconj  19314  f1otrspeq  19315  symggen  19338  psgnunilem1  19361  dprdf1o  19902  znleval  21110  znunithash  21120  mdetdiaglem  22100  basqtop  23215  tgqtop  23216  reghmph  23297  ordthmeolem  23305  qtophmeo  23321  imasf1oxmet  23881  imasf1omet  23882  imasf1obl  23997  imasf1oxms  23998  cnheiborlem  24470  ovolctb  25007  mbfimaopnlem  25172  logblog  26297  axcontlem5  28226  nvinvfval  29893  adjbd1o  31338  isoun  31923  fsumiunle  32035  symgcom  32244  pmtrcnel  32250  psgnfzto1stlem  32259  tocycfvres1  32269  tocycfvres2  32270  cycpmfvlem  32271  cycpmfv3  32274  cycpmconjvlem  32300  cycpmrn  32302  cycpmconjslem2  32314  indf1ofs  33024  esumiun  33092  eulerpartgbij  33371  eulerpartlemgh  33377  ballotlemsima  33514  derangenlem  34162  subfacp1lem3  34173  subfacp1lem4  34174  subfacp1lem5  34175  fv1stcnv  34748  fv2ndcnv  34749  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem9  36497  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem23  36511  ltrnid  39006  ltrneq2  39019  cdleme51finvN  39427  diaintclN  39929  dibintclN  40038  mapdcl  40524  kelac1  41805  gicabl  41841  brco2f1o  42783  brco3f1o  42784  ntrclsfv1  42806  ntrneifv1  42830  clsneikex  42857  clsneinex  42858  neicvgmex  42868  neicvgel1  42870  stoweidlem27  44743  isomushgr  46494  isomuspgrlem1  46495  isomuspgrlem2b  46497  isomuspgrlem2d  46499  isomuspgr  46502  isomgrtrlem  46506