Theorem f1ofn 6701

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

Syntax hints:   → wi 4   Fn wfn 6413  –1-1-onto→wf1o 6417

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 396  df-f 6422  df-f1 6423  df-f1o 6425

This theorem is referenced by:  f1ofun  6702  f1odm  6704  fveqf1o  7155  f1ofvswap  7158  isomin  7188  isoini  7189  isofrlem  7191  isoselem  7192  weniso  7205  bren  8701  brenOLD  8702  enfixsn  8821  phplem4  8895  php3  8899  dif1enlem  8905  f1oenfi  8926  f1oenfirn  8927  f1domfi  8928  domunfican  9017  fiint  9021  supisolem  9162  ordiso2  9204  unxpwdom2  9277  wemapwe  9385  djuun  9615  infxpenlem  9700  ackbij2lem2  9927  ackbij2lem3  9928  fpwwe2lem8  10325  canthp1lem2  10340  hashfacen  14094  hashfacenOLD  14095  hashf1lem1  14096  hashf1lem1OLD  14097  fprodss  15586  phimullem  16408  unbenlem  16537  0ram  16649  symgfixelsi  18958  symgfixf1  18960  f1omvdmvd  18966  f1omvdcnv  18967  f1omvdconj  18969  f1otrspeq  18970  symggen  18993  psgnunilem1  19016  dprdf1o  19550  znleval  20674  znunithash  20684  mdetdiaglem  21655  basqtop  22770  tgqtop  22771  reghmph  22852  ordthmeolem  22860  qtophmeo  22876  imasf1oxmet  23436  imasf1omet  23437  imasf1obl  23550  imasf1oxms  23551  cnheiborlem  24023  ovolctb  24559  mbfimaopnlem  24724  logblog  25847  axcontlem5  27239  nvinvfval  28903  adjbd1o  30348  isoun  30936  fsumiunle  31045  symgcom  31254  pmtrcnel  31260  psgnfzto1stlem  31269  tocycfvres1  31279  tocycfvres2  31280  cycpmfvlem  31281  cycpmfv3  31284  cycpmconjvlem  31310  cycpmrn  31312  cycpmconjslem2  31324  indf1ofs  31894  esumiun  31962  eulerpartgbij  32239  eulerpartlemgh  32245  ballotlemsima  32382  derangenlem  33033  subfacp1lem3  33044  subfacp1lem4  33045  subfacp1lem5  33046  fv1stcnv  33657  fv2ndcnv  33658  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem23  35727  ltrnid  38076  ltrneq2  38089  cdleme51finvN  38497  diaintclN  38999  dibintclN  39108  mapdcl  39594  kelac1  40804  gicabl  40840  brco2f1o  41531  brco3f1o  41532  ntrclsfv1  41554  ntrneifv1  41578  clsneikex  41605  clsneinex  41606  neicvgmex  41616  neicvgel1  41618  stoweidlem27  43458  isomushgr  45166  isomuspgrlem1  45167  isomuspgrlem2b  45169  isomuspgrlem2d  45171  isomuspgr  45174  isomgrtrlem  45178