Theorem f1of 5266

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 5265	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
2		f1f 5229	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ⟶wf 5024  –1-1→wf1 5025  –1-1-onto→wf1o 5027

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f1 5033  df-f1o 5035

This theorem is referenced by:  f1ofn  5267  f1oabexg  5278  f1ompt  5464  f1oresrab  5477  fsn  5483  fsnunf  5511  f1ocnvfv1  5570  f1ocnvfv2  5571  f1ocnvdm  5574  fcof1o  5582  isocnv  5604  isores2  5606  isotr  5609  isopolem  5615  isosolem  5617  f1oiso2  5620  f1ofveu  5654  smoiso  6081  mapsn  6461  f1oen2g  6526  en1  6570  enm  6590  mapen  6616  fidceq  6639  dif1en  6649  fin0  6655  fin0or  6656  ac6sfi  6668  en2eqpr  6677  fiintim  6693  isotilem  6755  supisoex  6758  supisoti  6759  ordiso2  6782  djuin  6810  caseinl  6836  ctm  6845  enomnilem  6855  frecuzrdgg  9884  fnn0nninf  9904  fxnn0nninf  9905  0tonninf  9906  1tonninf  9907  iseqf1olemkle  9974  iseqf1olemklt  9975  iseqf1olemqcl  9976  iseqf1olemnab  9978  iseqf1olemmo  9982  iseqf1olemqk  9984  iseqf1olemjpcl  9985  iseqf1olemfvp  9987  seq3f1olemqsumkj  9988  seq3f1olemqsumk  9989  seq3f1olemqsum  9990  seq3f1olemstep  9991  seq3f1olemp  9992  seq3f1oleml  9993  seq3f1o  9994  hashfz1  10252  omgadd  10271  hashfacen  10302  leisorel  10303  zfz1isolemiso  10305  iseqcoll  10308  cnrecnv  10405  sumeq2  10809  isummolem3  10831  isummolem2a  10832  fsumgcl  10838  fisum  10839  fsumf1o  10843  fisumss  10845  fsumcl2lem  10853  fsumadd  10861  fsummulc2  10903  sqpweven  11492  2sqpwodd  11493  phimullem  11540