Theorem f1ofn 6717

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

Syntax hints:   → wi 4   Fn wfn 6428  –1-1-onto→wf1o 6432

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 397  df-f 6437  df-f1 6438  df-f1o 6440

This theorem is referenced by:  f1ofun  6718  f1odm  6720  fveqf1o  7175  f1ofvswap  7178  isomin  7208  isoini  7209  isofrlem  7211  isoselem  7212  weniso  7225  bren  8743  brenOLD  8744  enfixsn  8868  dif1enlem  8943  f1oenfi  8965  f1oenfirn  8966  f1domfi  8967  phplem2  8991  php3  8995  phplem4OLD  9003  php3OLD  9007  domunfican  9087  fiint  9091  supisolem  9232  ordiso2  9274  unxpwdom2  9347  wemapwe  9455  djuun  9684  infxpenlem  9769  ackbij2lem2  9996  ackbij2lem3  9997  fpwwe2lem8  10394  canthp1lem2  10409  hashfacen  14166  hashfacenOLD  14167  hashf1lem1  14168  hashf1lem1OLD  14169  fprodss  15658  phimullem  16480  unbenlem  16609  0ram  16721  symgfixelsi  19043  symgfixf1  19045  f1omvdmvd  19051  f1omvdcnv  19052  f1omvdconj  19054  f1otrspeq  19055  symggen  19078  psgnunilem1  19101  dprdf1o  19635  znleval  20762  znunithash  20772  mdetdiaglem  21747  basqtop  22862  tgqtop  22863  reghmph  22944  ordthmeolem  22952  qtophmeo  22968  imasf1oxmet  23528  imasf1omet  23529  imasf1obl  23644  imasf1oxms  23645  cnheiborlem  24117  ovolctb  24654  mbfimaopnlem  24819  logblog  25942  axcontlem5  27336  nvinvfval  29002  adjbd1o  30447  isoun  31034  fsumiunle  31143  symgcom  31352  pmtrcnel  31358  psgnfzto1stlem  31367  tocycfvres1  31377  tocycfvres2  31378  cycpmfvlem  31379  cycpmfv3  31382  cycpmconjvlem  31408  cycpmrn  31410  cycpmconjslem2  31422  indf1ofs  31994  esumiun  32062  eulerpartgbij  32339  eulerpartlemgh  32345  ballotlemsima  32482  derangenlem  33133  subfacp1lem3  33144  subfacp1lem4  33145  subfacp1lem5  33146  fv1stcnv  33751  fv2ndcnv  33752  poimirlem1  35778  poimirlem2  35779  poimirlem3  35780  poimirlem4  35781  poimirlem6  35783  poimirlem7  35784  poimirlem8  35785  poimirlem9  35786  poimirlem13  35790  poimirlem14  35791  poimirlem15  35792  poimirlem16  35793  poimirlem17  35794  poimirlem19  35796  poimirlem20  35797  poimirlem23  35800  ltrnid  38149  ltrneq2  38162  cdleme51finvN  38570  diaintclN  39072  dibintclN  39181  mapdcl  39667  kelac1  40888  gicabl  40924  brco2f1o  41642  brco3f1o  41643  ntrclsfv1  41665  ntrneifv1  41689  clsneikex  41716  clsneinex  41717  neicvgmex  41727  neicvgel1  41729  stoweidlem27  43568  isomushgr  45278  isomuspgrlem1  45279  isomuspgrlem2b  45281  isomuspgrlem2d  45283  isomuspgr  45286  isomgrtrlem  45290