Theorem f1f 3662

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 3192	. 2 |- (F:A-1-1->B <-> (F:A-->B /\ Fun `'F))
2	1	pm3.26bi 322	1 |- (F:A-1-1->B -> F:A-->B)

Syntax hints:   -> wi 3  `'ccnv 3166  Fun wfun 3173  -->wf 3175  -1-1->wf1 3176

This theorem is referenced by:  f1of 3686  f1o5 3694  f1f1orn 3696  f1dmex 3707  brdomg 4371  f1domg 4390  2dom 4421  xpdom2 4435  fodomr 4476  inf3lem7 4606  unidom 4795

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-f1 3192

Copyright terms: Public domain