Theorem f1of1 2799

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

Assertion

Ref	Expression
f1of1	⊢ (F:A–1-1-onto→B → F:A–1-1→B)

Proof of Theorem f1of1

Step	Hyp	Ref	Expression
1		df-f1o 2437	. 2 ⊢ (F:A–1-1-onto→B ↔ (F:A–1-1→B ∧ F:A–onto→B))
2	1	pm3.26bd 259	1 ⊢ (F:A–1-1-onto→B → F:A–1-1→B)

Syntax hints:   → wi 2  –1-1→wf1 2419  –onto→wfo 2420  –1-1-onto→wf1o 2421

This theorem is referenced by:  f1of 2800  isowe 2941  f1oiso 2942  enssdom 3287  mapenlem2 3385  ssenen 3399  phplem5 3407  php3 3411  ssfi 3430  fiint 3445  infxpidmlem7 4939

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-f1o 2437

metamath.org