Theorem f1ofn 5822

Description: A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1ofn

Proof of Theorem f1ofn

Step	Hyp	Ref	Expression
1		f1of 5821	. 2
2		ffn 5736	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  Fnwfn 5588  -->wf 5589  -1-1-onto->wf1o 5592

This theorem is referenced by:  f1ofun  5823  f1odm  5825  fveqf1o  6205  isomin  6233  isoini  6234  isofrlem  6236  isoselem  6237  weniso  6250  bren  7545  enfixsn  7646  phplem4  7719  php3  7723  domunfican  7813  fiint  7817  supisolem  7952  ordiso2  7961  unxpwdom2  8035  wemapwe  8160  wemapweOLD  8161  infxpenlem  8412  ackbij2lem2  8641  ackbij2lem3  8642  fpwwe2lem9  9037  canthp1lem2  9052  hashfacen  12503  hashf1lem1  12504  fprodss  13755  phimullem  14309  unbenlem  14426  0ram  14538  symgfixelsi  16460  symgfixf1  16462  f1omvdmvd  16468  f1omvdcnv  16469  f1omvdconj  16471  f1otrspeq  16472  symggen  16495  psgnunilem1  16518  dprdf1o  17079  znleval  18593  znunithash  18603  mdetdiaglem  19100  basqtop  20212  tgqtop  20213  reghmph  20294  ordthmeolem  20302  qtophmeo  20318  imasf1oxmet  20878  imasf1omet  20879  imasf1obl  20991  imasf1oxms  20992  cnheiborlem  21454  ovolctb  21901  mbfimaopnlem  22062  axcontlem5  24271  vdgr1d  24903  vdgr1b  24904  vdgr1a  24906  eupai  24967  eupatrl  24968  eupap1  24976  eupath2lem3  24979  vdegp1ai  24984  vdegp1bi  24985  nvinvfval  25535  adjbd1o  27004  isoun  27520  indf1ofs  28039  eulerpartgbij  28311  eulerpartlemgh  28317  ballotlemsima  28454  derangenlem  28615  subfacp1lem3  28626  subfacp1lem4  28627  subfacp1lem5  28628  kelac1  31009  gicabl  31047  stoweidlem27  31809  usgra2adedglem1  32356  ltrnid  35859  ltrneq2  35872  cdleme51finvN  36282  diaintclN  36785  dibintclN  36894  mapdcl  37380

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 185  df-an 371  df-f 5597  df-f1 5598  df-f1o 5600