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