Theorem f1of 5146

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

Assertion

Ref	Expression
f1of	⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Proof of Theorem f1of

Step	Hyp	Ref	Expression
1		f1of1 5145	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
2		f1f 5112	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ⟶wf 4918  –1-1→wf1 4919  –1-1-onto→wf1o 4921

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 4927  df-f1o 4929

This theorem is referenced by:  f1ofn  5147  f1oabexg  5158  f1ompt  5341  f1oresrab  5350  fsn  5356  fsnunf  5383  f1ocnvfv1  5437  f1ocnvfv2  5438  f1ocnvdm  5441  fcof1o  5449  isocnv  5471  isores2  5473  isotr  5476  isopolem  5481  isosolem  5483  f1oiso2  5486  f1ofveu  5520  smoiso  5940  f1oen2g  6258  en1  6302  enm  6317  fidceq  6354  dif1en  6364  fin0  6369  fin0or  6370  ac6sfi  6379  en2eqpr  6380  isotilem  6419  supisoex  6422  supisoti  6423  ordiso2  6446  cnrecnv  9797  sqpweven  10553  2sqpwodd  10554