Theorem f1of 5157

Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of	|- ( F : A -1-1-onto-> B -> F : A --> B )

Proof of Theorem f1of

Step	Hyp	Ref	Expression
1		f1of1 5156	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5123	. 2 |- ( F : A -1-1-> B -> F : A --> B )
3	1, 2	syl 14	1 |- ( F : A -1-1-onto-> B -> F : A --> B )

Syntax hints:   -> wi 4   -->wf 4928   -1-1->wf1 4929   -1-1-onto->wf1o 4931

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115  df-f1 4937  df-f1o 4939

This theorem is referenced by:  f1ofn  5158  f1oabexg  5169  f1ompt  5352  f1oresrab  5361  fsn  5367  fsnunf  5394  f1ocnvfv1  5448  f1ocnvfv2  5449  f1ocnvdm  5452  fcof1o  5460  isocnv  5482  isores2  5484  isotr  5487  isopolem  5492  isosolem  5494  f1oiso2  5497  f1ofveu  5531  smoiso  5951  f1oen2g  6302  en1  6346  enm  6364  fidceq  6404  dif1en  6414  fin0  6419  fin0or  6420  ac6sfi  6431  en2eqpr  6434  isotilem  6478  supisoex  6481  supisoti  6482  ordiso2  6505  frecuzrdgg  9498  sizefz1  9807  omgadd  9826  cnrecnv  9935  sumeq2d  10334  sumeq2  10335  sqpweven  10697  2sqpwodd  10698