Theorem f1f 2781

Description: A one-to-one mapping is a mapping.

Assertion

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

Proof of Theorem f1f

Step	Hyp	Ref	Expression
1		df-f1 2435	. 2 |- (F:A-1-1->B <-> (F:A-->B /\ Fun `'F))
2	1	pm3.26bd 259	1 |- (F:A-1-1->B -> F:A-->B)

Syntax hints:   -> wi 2  `'ccnv 2409  Fun wfun 2416  -->wf 2418  -1-1->wf1 2419

This theorem is referenced by:  f1of 2800  f1o5 2808  f1f1orn 2810  f1dmex 2819  brdomg 3281  f1domg 3299  2dom 3332  xpdom2 3345  inf3lem7 3470  fodomb 3615

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-f1 2435

metamath.org