Theorem f1ofn 6832

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

Syntax hints:   → wi 4   Fn wfn 6536  –1-1-onto→wf1o 6540

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 6545  df-f1 6546  df-f1o 6548

This theorem is referenced by:  f1ofun  6833  f1odm  6835  fveqf1o  7298  f1ofvswap  7301  isomin  7331  isoini  7332  isofrlem  7334  isoselem  7335  weniso  7348  bren  8946  brenOLD  8947  enfixsn  9078  dif1enlem  9153  dif1enlemOLD  9154  f1oenfi  9179  f1oenfirn  9180  f1domfi  9181  phplem2  9205  php3  9209  phplem4OLD  9217  php3OLD  9221  domunfican  9317  fiint  9321  supisolem  9465  ordiso2  9507  unxpwdom2  9580  wemapwe  9689  djuun  9918  infxpenlem  10005  ackbij2lem2  10232  ackbij2lem3  10233  fpwwe2lem8  10630  canthp1lem2  10645  hashfacen  14410  hashfacenOLD  14411  hashf1lem1  14412  hashf1lem1OLD  14413  fprodss  15889  phimullem  16709  unbenlem  16838  0ram  16950  symgfixelsi  19298  symgfixf1  19300  f1omvdmvd  19306  f1omvdcnv  19307  f1omvdconj  19309  f1otrspeq  19310  symggen  19333  psgnunilem1  19356  dprdf1o  19897  znleval  21102  znunithash  21112  mdetdiaglem  22092  basqtop  23207  tgqtop  23208  reghmph  23289  ordthmeolem  23297  qtophmeo  23313  imasf1oxmet  23873  imasf1omet  23874  imasf1obl  23989  imasf1oxms  23990  cnheiborlem  24462  ovolctb  24999  mbfimaopnlem  25164  logblog  26287  axcontlem5  28216  nvinvfval  29881  adjbd1o  31326  isoun  31911  fsumiunle  32023  symgcom  32232  pmtrcnel  32238  psgnfzto1stlem  32247  tocycfvres1  32257  tocycfvres2  32258  cycpmfvlem  32259  cycpmfv3  32262  cycpmconjvlem  32288  cycpmrn  32290  cycpmconjslem2  32302  indf1ofs  33013  esumiun  33081  eulerpartgbij  33360  eulerpartlemgh  33366  ballotlemsima  33503  derangenlem  34151  subfacp1lem3  34162  subfacp1lem4  34163  subfacp1lem5  34164  fv1stcnv  34737  fv2ndcnv  34738  poimirlem1  36478  poimirlem2  36479  poimirlem3  36480  poimirlem4  36481  poimirlem6  36483  poimirlem7  36484  poimirlem8  36485  poimirlem9  36486  poimirlem13  36490  poimirlem14  36491  poimirlem15  36492  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem23  36500  ltrnid  38995  ltrneq2  39008  cdleme51finvN  39416  diaintclN  39918  dibintclN  40027  mapdcl  40513  kelac1  41791  gicabl  41827  brco2f1o  42769  brco3f1o  42770  ntrclsfv1  42792  ntrneifv1  42816  clsneikex  42843  clsneinex  42844  neicvgmex  42854  neicvgel1  42856  stoweidlem27  44730  isomushgr  46481  isomuspgrlem1  46482  isomuspgrlem2b  46484  isomuspgrlem2d  46486  isomuspgr  46489  isomgrtrlem  46493