Theorem f1fn 5787

Description: A one-to-one mapping is a function on its domain. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1fn

Proof of Theorem f1fn

Step	Hyp	Ref	Expression
1		f1f 5786	. 2
2		ffn 5736	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590

This theorem is referenced by:  f1fun  5788  f1rel  5789  f1dm  5790  f1ssr  5792  f1f1orn  5832  f1elima  6171  f1eqcocnv  6204  domunsncan  7637  marypha2  7919  infdifsn  8094  acndom  8453  dfac12lem2  8545  ackbij1  8639  fin23lem32  8745  fin1a2lem5  8805  fin1a2lem6  8806  pwfseqlem1  9057  hashf1lem1  12504  hashf1  12506  odf1o2  16593  kerf1hrm  17392  frlmlbs  18831  f1lindf  18857  2ndcdisj  19957  qtopf1  20317  usgraedgrn  24381  usgfidegfi  24910  erdszelem10  28644  dihfn  36995  dihcl  36997  dih1dimatlem  37056  dochocss  37093

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