Theorem f1of 5507

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

Syntax hints:   → wi 4  ⟶wf 5255  –1-1→wf1 5256  –1-1-onto→wf1o 5258

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

This theorem depends on definitions:  df-bi 117  df-f1 5264  df-f1o 5266

This theorem is referenced by:  f1ofn  5508  f1oabexg  5519  f1ompt  5716  f1oresrab  5730  fsn  5737  fsnunf  5765  f1ocnvfv1  5827  f1ocnvfv2  5828  f1ocnvdm  5831  fcof1o  5839  isocnv  5861  isores2  5863  isotr  5866  isopolem  5872  isosolem  5874  f1oiso2  5877  f1ofveu  5913  smoiso  6369  mapsn  6758  f1oen2g  6823  en1  6867  enm  6888  mapen  6916  fidceq  6939  dif1en  6949  fin0  6955  fin0or  6956  ac6sfi  6968  en2eqpr  6977  fiintim  7001  isotilem  7081  supisoex  7084  supisoti  7085  ordiso2  7110  caseinl  7166  caseinr  7167  omp1eomlem  7169  ctm  7184  enomnilem  7213  enmkvlem  7236  enwomnilem  7244  cc3  7351  frecuzrdgg  10525  fnn0nninf  10547  fxnn0nninf  10548  0tonninf  10549  1tonninf  10550  iseqf1olemkle  10606  iseqf1olemklt  10607  iseqf1olemqcl  10608  iseqf1olemnab  10610  iseqf1olemmo  10614  iseqf1olemqk  10616  iseqf1olemjpcl  10617  iseqf1olemfvp  10619  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  seq3f1olemstep  10623  seq3f1olemp  10624  seq3f1oleml  10625  seq3f1o  10626  seqf1oglem1  10628  seqf1oglem2  10629  seqf1og  10630  hashfz1  10892  omgadd  10911  hashfacen  10945  leisorel  10946  zfz1isolemiso  10948  seq3coll  10951  cnrecnv  11092  sumeq2  11541  summodclem3  11562  summodclem2a  11563  fsumgcl  11568  fsum3  11569  fsumf1o  11572  fisumss  11574  fsumcl2lem  11580  fsumadd  11588  fsummulc2  11630  prodeq2  11739  prodmodclem3  11757  prodmodclem2a  11758  fprodseq  11765  fprodf1o  11770  fprodssdc  11772  fprodmul  11773  nninfctlemfo  12232  sqpweven  12368  2sqpwodd  12369  phimullem  12418  eulerthlem1  12420  eulerthlemrprm  12422  eulerthlema  12423  eulerthlemh  12424  eulerthlemth  12425  ennnfonelemjn  12644  ennnfonelemp1  12648  ennnfonelemhdmp1  12651  ennnfonelemss  12652  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemex  12656  ennnfonelemnn0  12664  ennnfonelemim  12666  ctinfomlemom  12669  ctiunctlemudc  12679  ctiunctlemfo  12681  ssnnctlemct  12688  idmhm  13171  mhmf1o  13172  idghm  13465  ghmf1o  13481  gsumfzreidx  13543  psrnegcl  14311  psrlinv  14312  ssidcn  14530  txhmeo  14639  dvid  15015  dvidre  15017  dvexp  15031  dfrelog  15180  relogcl  15182  012of  15724  2o01f  15725  iswomninnlem  15780